LEAN 类型理论之注解(Annotations of LEAN Type Theory)—— 定义上相等(Definitional Equality)

本文主要是介绍LEAN 类型理论之注解(Annotations of LEAN Type Theory)—— 定义上相等(Definitional Equality),希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

        定义上相等(Definitional Equality)指的是意义上相等,即同义,包括了,定义的缩写(Abbreviatory Definition),alpha转换,相同替代(substituting equals for equals)等。下面是LEAN给定的何谓 定义上相等。 

        注:罗列的推演规则中,如自明其义的,则不多加解析其前提、结果、或特定注解。

         一、表达式的定义上相等(Definitional Equality of Expressions)(Γ ⊢ e₁ ≡ e₂)

1. 定义上相等的自反性(Reflexive)

前提(Premises):

        a. 在 Γ  的假设,表达式 e 的类型是 α。

结果(Conclusion):

        在 Γ  的假设,表达式 e 定义上等于表达式 e 自己。

2. 定义上相等的互换性(Commutive)

3. 定义上相等的传递性(Transitive)

4. 类型宇宙的定义上相等(Definitional Equality for Universes)

5. 函数应用的同义替换(Substituting equals for equals in Application Typing Rule)

6. 抽象化的同义替换(Substituting equals for equals in Abstraction Typing Rule)

7. 依赖函数类型的同义替换(Substituting equals for equals in Dependent Function Type)

8. Beta 简化 (Beta Reduction)

        注解:

                该推演规则定义了,LEAN的Beta简化,即,函数应用(Function application, or application in short) 在定义上相等于(Definitional equals)函数体的表达式 e 中,将所有输入变量替换成调用时输入的表达式 e'。

9. Eta 简化(Eta Reduction)

        注解:

                该推演规则定义了,LEAN的 Eta简化,即,对已有的函数 e 再抽象化,定义上相等于(Definitional equals)其自己 e (itself)。

10. 证明无关性(Proof Irrelevance)

前提(Premises):

        a. 在 Γ  的假设,类型表达式 p 存在于类型宇宙 ℙ,即 p 是一个命题,ℙ 为命题类型宇宙。

        b. 在 Γ  的假设,表达式 h 的类型为 类型表达式 p,即 h 证明了 p。

        c. 在 Γ  的假设,表达式 h' 的类型为 类型表达式 p,即 h' 证明了 p。

结果(Conclusion):

        在 Γ  的假设,表达式 h 定义上等于表达式 h' 。

注解:

        该推演规则定义了,如果两个不同的证据(proof),h 和 h',证明了同样的命题 p,那么这两个证据在定义上相等(Definitional equals)。

二、宇宙层次的定义上相等(Definitional Equality of Levels)

        宇宙层次的定义上相等通过不等式来定义,即 𝑙 ≤ 𝑙' + n, n ∈ ℤ,当 n = 0时,𝑙 ≤ 𝑙'。另外在其论文有简要的说明,如何理解这个宇宙层次,这里就直接引用了。

        然后,再分别对每条推演规则进行注解。

1. 宇宙层次的定义上相等 (Definitional Equality of Levels)(𝑙 ≡ 𝑙')

2. 宇宙层次必须大于等0

3. 宇宙层次大于等于自身

4. 定义不等式左边的下一级的宇宙层次

        注解:当前宇宙层次 𝑙 ,另一宇宙层次 𝑙‘,有 𝑙 ≤ 𝑙‘ + (n - 1),那么,当前宇宙层次 𝑙  的下一级宇宙层次 S𝑙 ,会有 S𝑙 ≤ 𝑙‘ + (n - 1) + 1,即 S𝑙  ≤ 𝑙‘ + n 。也就是说,S𝑙 是 𝑙 层次的递进 1 级(+1)。

5. 定义不等式右边的下一级的宇宙层次

        注解:定义在不等式右边的,S𝑙'  ≡ 𝑙' + 1

6. 定义 作用在宇宙层次的 max函数 和 imax 函数

        注解:当  𝑙₁ + n  或  𝑙₂ + n 大于等于  𝑙,不管 𝑙₁ 和 𝑙₂ 谁的值大,其 max(𝑙₁, 𝑙₂) 都是获取其中的最大值,因此, max(𝑙₁, 𝑙₂) + n 必然 大于等于 𝑙。上面两个推演规则说明了,max函数内的左右输入的位置不影响其输出的结果。

        注解:当max函数的左右输入都小于等于  𝑙 + n 时,那么其结果也小于等于  𝑙 + n,即 max 只获取左右输入的较大值,而不增减其宇宙层次。

        注解:当 imax函数的右输入为层次 0 时,其输出亦为 0 。即,imax 函数的左右输入需要严格区分,会影响其输出的结果。

        注解:当 imax函数的右输入不等于 0 时,即 S𝑙₂,必大于0,其等价于max函数。

        注解:由于imax函数对其右输入是否为0敏感,因此,分析上面两条推演规则,即不等式左右两边的max函数与imax函数的关系,时,可按情况分别分析 𝑙₃ 是否等于 0。

        注释:这里突出了 𝑙 是宇宙层次表达式,其中可含有宇宙层次变量 u,在实际使用的过程中,其变量会被替换成实际的自然数值。

这篇关于LEAN 类型理论之注解(Annotations of LEAN Type Theory)—— 定义上相等(Definitional Equality)的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/1137097

相关文章

Java 中的 @SneakyThrows 注解使用方法(简化异常处理的利与弊)

《Java中的@SneakyThrows注解使用方法(简化异常处理的利与弊)》为了简化异常处理,Lombok提供了一个强大的注解@SneakyThrows,本文将详细介绍@SneakyThro... 目录1. @SneakyThrows 简介 1.1 什么是 Lombok?2. @SneakyThrows

Java Spring 中 @PostConstruct 注解使用原理及常见场景

《JavaSpring中@PostConstruct注解使用原理及常见场景》在JavaSpring中,@PostConstruct注解是一个非常实用的功能,它允许开发者在Spring容器完全初... 目录一、@PostConstruct 注解概述二、@PostConstruct 注解的基本使用2.1 基本代

Java中的@SneakyThrows注解用法详解

《Java中的@SneakyThrows注解用法详解》:本文主要介绍Java中的@SneakyThrows注解用法的相关资料,Lombok的@SneakyThrows注解简化了Java方法中的异常... 目录前言一、@SneakyThrows 简介1.1 什么是 Lombok?二、@SneakyThrows

C 语言中enum枚举的定义和使用小结

《C语言中enum枚举的定义和使用小结》在C语言里,enum(枚举)是一种用户自定义的数据类型,它能够让你创建一组具名的整数常量,下面我会从定义、使用、特性等方面详细介绍enum,感兴趣的朋友一起看... 目录1、引言2、基本定义3、定义枚举变量4、自定义枚举常量的值5、枚举与switch语句结合使用6、枚

SpringRetry重试机制之@Retryable注解与重试策略详解

《SpringRetry重试机制之@Retryable注解与重试策略详解》本文将详细介绍SpringRetry的重试机制,特别是@Retryable注解的使用及各种重试策略的配置,帮助开发者构建更加健... 目录引言一、SpringRetry基础知识二、启用SpringRetry三、@Retryable注解

SpringValidation数据校验之约束注解与分组校验方式

《SpringValidation数据校验之约束注解与分组校验方式》本文将深入探讨SpringValidation的核心功能,帮助开发者掌握约束注解的使用技巧和分组校验的高级应用,从而构建更加健壮和可... 目录引言一、Spring Validation基础架构1.1 jsR-380标准与Spring整合1

SpringBoot条件注解核心作用与使用场景详解

《SpringBoot条件注解核心作用与使用场景详解》SpringBoot的条件注解为开发者提供了强大的动态配置能力,理解其原理和适用场景是构建灵活、可扩展应用的关键,本文将系统梳理所有常用的条件注... 目录引言一、条件注解的核心机制二、SpringBoot内置条件注解详解1、@ConditionalOn

MySQL 中查询 VARCHAR 类型 JSON 数据的问题记录

《MySQL中查询VARCHAR类型JSON数据的问题记录》在数据库设计中,有时我们会将JSON数据存储在VARCHAR或TEXT类型字段中,本文将详细介绍如何在MySQL中有效查询存储为V... 目录一、问题背景二、mysql jsON 函数2.1 常用 JSON 函数三、查询示例3.1 基本查询3.2

SpringBoot利用@Validated注解优雅实现参数校验

《SpringBoot利用@Validated注解优雅实现参数校验》在开发Web应用时,用户输入的合法性校验是保障系统稳定性的基础,​SpringBoot的@Validated注解提供了一种更优雅的解... 目录​一、为什么需要参数校验二、Validated 的核心用法​1. 基础校验2. php分组校验3

Pydantic中Optional 和Union类型的使用

《Pydantic中Optional和Union类型的使用》本文主要介绍了Pydantic中Optional和Union类型的使用,这两者在处理可选字段和多类型字段时尤为重要,文中通过示例代码介绍的... 目录简介Optional 类型Union 类型Optional 和 Union 的组合总结简介Pyd