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

相关文章

Spring事务中@Transactional注解不生效的原因分析与解决

《Spring事务中@Transactional注解不生效的原因分析与解决》在Spring框架中,@Transactional注解是管理数据库事务的核心方式,本文将深入分析事务自调用的底层原理,解释为... 目录1. 引言2. 事务自调用问题重现2.1 示例代码2.2 问题现象3. 为什么事务自调用会失效3

Java常用注解扩展对比举例详解

《Java常用注解扩展对比举例详解》:本文主要介绍Java常用注解扩展对比的相关资料,提供了丰富的代码示例,并总结了最佳实践建议,帮助开发者更好地理解和应用这些注解,需要的朋友可以参考下... 目录一、@Controller 与 @RestController 对比二、使用 @Data 与 不使用 @Dat

基于@RequestParam注解之Spring MVC参数绑定的利器

《基于@RequestParam注解之SpringMVC参数绑定的利器》:本文主要介绍基于@RequestParam注解之SpringMVC参数绑定的利器,具有很好的参考价值,希望对大家有所帮助... 目录@RequestParam注解:Spring MVC参数绑定的利器什么是@RequestParam?@

Python如何查看数据的类型

《Python如何查看数据的类型》:本文主要介绍Python如何查看数据的类型方式,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录python查看数据的类型1. 使用 type()2. 使用 isinstance()3. 检查对象的 __class__ 属性4.

Python容器类型之列表/字典/元组/集合方式

《Python容器类型之列表/字典/元组/集合方式》:本文主要介绍Python容器类型之列表/字典/元组/集合方式,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录1. 列表(List) - 有序可变序列1.1 基本特性1.2 核心操作1.3 应用场景2. 字典(D

Python如何在Word中生成多种不同类型的图表

《Python如何在Word中生成多种不同类型的图表》Word文档中插入图表不仅能直观呈现数据,还能提升文档的可读性和专业性,本文将介绍如何使用Python在Word文档中创建和自定义各种图表,需要的... 目录在Word中创建柱形图在Word中创建条形图在Word中创建折线图在Word中创建饼图在Word

SpringBoot接收JSON类型的参数方式

《SpringBoot接收JSON类型的参数方式》:本文主要介绍SpringBoot接收JSON类型的参数方式,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录一、jsON二、代码准备三、Apifox操作总结一、JSON在学习前端技术时,我们有讲到过JSON,而在

Spring Security注解方式权限控制过程

《SpringSecurity注解方式权限控制过程》:本文主要介绍SpringSecurity注解方式权限控制过程,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录一、摘要二、实现步骤2.1 在配置类中添加权限注解的支持2.2 创建Controller类2.3 Us

Java中使用注解校验手机号格式的详细指南

《Java中使用注解校验手机号格式的详细指南》在现代的Web应用开发中,数据校验是一个非常重要的环节,本文将详细介绍如何在Java中使用注解对手机号格式进行校验,感兴趣的小伙伴可以了解下... 目录1. 引言2. 数据校验的重要性3. Java中的数据校验框架4. 使用注解校验手机号格式4.1 @NotBl

SpringBoot自定义注解如何解决公共字段填充问题

《SpringBoot自定义注解如何解决公共字段填充问题》本文介绍了在系统开发中,如何使用AOP切面编程实现公共字段自动填充的功能,从而简化代码,通过自定义注解和切面类,可以统一处理创建时间和修改时间... 目录1.1 问题分析1.2 实现思路1.3 代码开发1.3.1 步骤一1.3.2 步骤二1.3.3