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

相关文章

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

Spring Security方法级安全控制@PreAuthorize注解的灵活运用小结

《SpringSecurity方法级安全控制@PreAuthorize注解的灵活运用小结》本文将带着大家讲解@PreAuthorize注解的核心原理、SpEL表达式机制,并通过的示例代码演示如... 目录1. 前言2. @PreAuthorize 注解简介3. @PreAuthorize 核心原理解析拦截与

Oracle数据库常见字段类型大全以及超详细解析

《Oracle数据库常见字段类型大全以及超详细解析》在Oracle数据库中查询特定表的字段个数通常需要使用SQL语句来完成,:本文主要介绍Oracle数据库常见字段类型大全以及超详细解析,文中通过... 目录前言一、字符类型(Character)1、CHAR:定长字符数据类型2、VARCHAR2:变长字符数

SpringCloud动态配置注解@RefreshScope与@Component的深度解析

《SpringCloud动态配置注解@RefreshScope与@Component的深度解析》在现代微服务架构中,动态配置管理是一个关键需求,本文将为大家介绍SpringCloud中相关的注解@Re... 目录引言1. @RefreshScope 的作用与原理1.1 什么是 @RefreshScope1.

Spring Boot 配置文件之类型、加载顺序与最佳实践记录

《SpringBoot配置文件之类型、加载顺序与最佳实践记录》SpringBoot的配置文件是灵活且强大的工具,通过合理的配置管理,可以让应用开发和部署更加高效,无论是简单的属性配置,还是复杂... 目录Spring Boot 配置文件详解一、Spring Boot 配置文件类型1.1 applicatio