黄的网站建设,如何做一元购物网站,互动平台有哪些,河南工程新希望官网《何谓相等 (Equality)#xff0c;在类型理论(Type Theory)语境下》 与 《转化#xff08;conversion and reduction#xff09;后的相等#xff08;Equality#xff09;》#xff0c;两文中#xff0c;已对相等#xff08;Equality#xff09;的概念进行了描述#… 《何谓相等 (Equality)在类型理论(Type Theory)语境下》 与 《转化conversion and reduction后的相等Equality》两文中已对相等Equality的概念进行了描述此文是LEAN中通过定义一个用于表达express相等equality的归纳类型Inductive Type即相等类型Equality Type。 相等类型Equality Type表达了给定一个类型 α类型α里的元素自身相等equals itself即其自反性reflexivity。记为 α:Uₗ, a:α ⊢ eqₐ : μt: α→ℙ .(refl: t a) 析 给定 类型α 及 类型为α 的变量 a有相等类型 eqₐ其定义为 μt: α→ℙ .(refl: t a)。 也就是说eqₐ 是类型函数α→ℙ输入为类型α 的值输出为命题proposition其构建函数为 refl: t a因 t 的类型为 α→ℙ有 t a eqₐ a其类型为 ℙ Proposition即 refl: eqₐ a :ℙ 为命题的证明proof of proposition。 也就是说给定一个类型 α 及该类型的变量 a有相等类型 eqₐ其含义为给定另一个类型 α的值 a 生成出一个判断Judgement / Propositiona 与 a 相等即 eqₐ a :ℙ 与其构建函数 refl 的类型eqₐ a :ℙ相同因此构建函数 refl用于构建该判断的证明proof。构建函数 refl的定义(refl: t a) 中的 a引用的是 ⊢ 符号左边的变量 a也是 eqₐ 中的 a因此构建函数 refl 表达了当 a 与 a 是同一个时两者相等即作为 eqₐ a :ℙ 的证明proof
refl: eqₐ a :ℙ refl: eqₐ a :ℙa a 关键点(refl: t a) 和 eqₐ 中的变量 a是同一个变量a来自其假设Assumptions即 ⊢ 符号左边的变量 a。 换个看法将相等类型看作 eq而非 eqₐ有 eq : α:Uₗ → a:α → b: α→ ℙ 即给定对应的输入eq 返回一个命题proposition, 即 a 与 b 相等。 其构建函数 refl short for reflexivity 是
refl: a:α → (eq α a a) 即其输入只有一个值来自 ⊢ 符号左边的变量 a说明了该值等于其自身即自反性reflexivity。 也就是说相等类型表达了只有任何类型的元素其自身相等reflexivity。 同时LEAN类型系统定义了定义上相等Definitioanl Equality的表示达可以相互替换substitute equals for equals由此当两个表达式通过使用各种转化规则最终规范化成相同元素则两个表达式相等即 eq a bwhere a⇔ b。 另外因相等类型只有一个无参数的构建函数refl: t a所以相等类型的使用函数是 Large Elimination即其使用函数的目标类型Target Type可以指向任意类型宇宙Universes。 使用 LEAN 语言的语法表达如下
inductive Eq : α → α → Prop where| refl (a : α) : Eq a a 注LEAN语言 是 LEAN类型理论中的表达式语法Syntax of Expression 的 具象化Embodiment用于在代码层级上表达 LEAN类型理论中定义的所有表达式Expression。
