对于lambda演算相信只要学过离散数学的基本上都是都在课上学习过了，简单的说这是一种使用替换来描述的非常好用的形式系统。不敢说非常懂这个东西，但是直观上我觉得这个东西和谓词逻辑在很多地方很像。 在离散里学这个的时候，我们说的叫做无类型lambda演算，在foundation里，需要研究一下更加复杂的简单类型lambda演算(Simply typed lambda calculus)。为了方便通称STLC。
类型系统的引入可以大大提高语义的准确性，而实际中的大多数以lambda演算为核心的编程语言中(函数式编程语言)，也有很多是有类型的，比如Haskell。当然Haskell的类型系统远远不是"Simple"的。
少女抄书中......
0X00 语法
接下来我们讨论这种简易的玩具语言中将使用以下语法:
- 基础类型(base type): bool类型 (为了方便，只添加bool类型，实际上其他的数字等都是可以加入的。)
- 常量： fls tru,真假两种布尔值
- 条件语句：test t1 then t2 else t3
- 变量
- 函数抽象：\x:T1.t2 .其中
\就是lambda演算中的字母,代表一个匿名的函数，
x是函数的参数，: T1是参数x的类型标注，t2是函数体 - 函数作用： t1 t2. 表示把t1 函数apply到t2上去
- 箭头类型： * -> * 函数的类型，和大多是函数式语言一样
Example
\x: Bool. x 一个输入x输出x的函数
(\x:Bool. x) tru 把上面定义的函数作用到参数true上
\x:Bool. test x then fls else tru 一个取反的函数
\f:Bool→Bool. f (f tru) 一个接受函数f作为参数的高阶函数
形式化的有：
Inductive ty : Type :=
| Bool : ty
| Arrow : ty → ty → ty.
Inductive tm : Type :=
| var : string → tm
| app : tm → tm → tm
| abs : string → ty → tm → tm
| tru : tm
| fls : tm
| test : tm → tm → tm → tm.
需要注意的是，在大多数主流语言中比如ML, Haskell中，存在类型推导，可以通过函数体去推测类型，但是为了方便讨论，我们定义的语言中参数的类型标注(type annotation)是不能省略的。
0X01操作语义
采用small-step操作语义
值(value)
- bool值tru, fls
- 函数作用，比如f a这样的，如果f是纯函数，那么f a确定的时候，值就已经确定了，所以所有的函数作用当然可以看成值
- 函数是值
需要注意的是，在主流的编程语言中，不管是什么函数一般都被看作一个值，但是Coq中并不是，只有函数体是值那么整个函数才是值。我们这里为了验证方便采用前一种方式。
完备(complete)
一个不出现自由变量(free varible)的程序，被称为完备程序(complete program)。换句话说一个完整的程序是封闭的(closed)。
我们当前讨论的语言就是完备程序，这其实是为了避开对变量到底是不是值的讨论，因为都是封闭项，所以变量只会出现在我们归约的过程当中。
替换(substitution)
lambda calculus的核心思想就是替换，在这里我们当然也需要在操作语义中使用替换。
来看一个简单的替换
(\x: Bool. x) tru
-----------------------
tru
这个应该不难理解，函数作用的过程本质就是把变量x替换为传给函数的参数。替换的过程可以用[x:=s]t表示，读作“把t中的x替换为s”
其实这个东西和谓词逻辑中的替换是非常相似的，下面这个例子也会更好的说明这一点。
[x:=tru] (\x:Bool. x)
------------------------
(\x:Bool. x)
是不是一下没有反应过来和第一个例子有什么不一样23333，第一个例子本质是[x:=tru]x.第二个例子中的x不是自由变量，他被lambda符号给capture了，或者说他是被绑定的(bound)！就好像在谓词逻辑中进行替换时候，被全称量词capture了，就不能被替换了，也是一个道理。替换只能针对自由变量。
ok,接下来是完整的替换法则
[x:=s]x = s
[x:=s]y = y if x ≠ y
[x:=s](\x:T11. t12) = \x:T11. t12
[x:=s](\y:T11. t12) = \y:T11. [x:=s]t12 if x ≠ y
[x:=s](t1 t2) = ([x:=s]t1) ([x:=s]t2)
[x:=s]tru = tru
[x:=s]fls = fls
[x:=s](test t1 then t2 else t3) =
test [x:=s]t1 then [x:=s]t2 else [x:=s]t3
形式化的有
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
| var x' ⇒
if eqb_string x x' then s else t
| abs x' T t1 ⇒
abs x' T (if eqb_string x x' then t1 else ([x:=s] t1))
| app t1 t2 ⇒
app ([x:=s] t1) ([x:=s] t2)
| tru ⇒
tru
| fls ⇒
fls
| test t1 t2 t3 ⇒
test ([x:=s] t1) ([x:=s] t2) ([x:=s] t3)
end
where "'[' x ':=' s ']' t" := (subst x s t).
这里还是有一个问题，如果我们替换的名字虽然没有被当前的环境capture但是比如在全局作用域中，这个名字已经绑定过了。。。这时候就尴尬了，因为我们的变量名应该是不能影响语义的，局部全局重名很麻烦，需要额外规定，现在的语义没考虑这一点。在这里为了方便，暂时不处理。
归约
之前说了，有了替换，我们就可以对于函数作用进行归约了，也就是我们在演算中的
-归约(beta-reduction):
(\x:T.t12) v2 --> [x:=v2]t12
非形式化的可以写成（我抽空写成）
value v2
------------------------------------
(\x:T.t12) v2 --> [x:=v2]t12
t1 --> t1'
------------------------------------
t1 t2 --> t1' t2
value v1
t2 --> t2'
------------------------------------
v1 t2 --> v1 t2'
------------------------------------
(test tru then t1 else t2) --> t1
------------------------------------
(test fls then t1 else t2) --> t2
t1 --> t1'
----------------------------------------------------------
(test t1 then t2 else t3) --> (test t1' then t2 else t3)
形式化的完整small step操作
Inductive step : tm → tm → Prop :=
| ST_AppAbs : ∀x T t12 v2,
value v2 →
(app (abs x T t12) v2) --> [x:=v2]t12
| ST_App1 : ∀t1 t1' t2,
t1 --> t1' →
app t1 t2 --> app t1' t2
| ST_App2 : ∀v1 t2 t2',
value v1 →
t2 --> t2' →
app v1 t2 --> app v1 t2'
| ST_TestTru : ∀t1 t2,
(test tru t1 t2) --> t1
| ST_TestFls : ∀t1 t2,
(test fls t1 t2) --> t2
| ST_Test : ∀t1 t1' t2 t3,
t1 --> t1' →
(test t1 t2 t3) --> (test t1' t2 t3)
where "t1 '-->' t2" := (step t1 t2).
Hint Constructors step.
Notation multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).
0X02 类型
Q : x y的类型是什么？
A： 这取决与x和y的类型是什么
也就是说，在STLC中我们单看符号是看不出两个符号有什么类型的，只有放到一个上下文(contex)中，才能讨论类型，ok,扩充一下我们的类型断言，记作
Gamma
t ∈ T
其中Gamma被称为类型上下文,读作“满足Gamma时，t 有类型 T”。
一般的我们用一个偏射来表示表示上下文， 因此，更新上下文的过程可以记作
(X
T1; Gamma)
靠直觉，来写一下
Reserved Notation "Gamma '⊢' t '∈' T" (at level 40).
Inductive has_type : context → tm → ty → Prop :=
| T_Var : ∀ Gamma x T,
Gamma x = Some T →
Gamma ⊢ var x ∈ T
| T_Abs : ∀ Gamma x T11 T12 t12,
(x ⊢> T11 ; Gamma) ⊢ t12 ∈ T12 →
Gamma ⊢ abs x T11 t12 ∈ Arrow T11 T12
| T_App : ∀ T11 T12 Gamma t1 t2,
Gamma ⊢ t1 ∈ Arrow T11 T12 →
Gamma ⊢ t2 ∈ T11 →
Gamma ⊢ app t1 t2 ∈ T12
| T_Tru : ∀ Gamma,
Gamma ⊢ tru ∈ Bool
| T_Fls : ∀ Gamma,
Gamma ⊢ fls ∈ Bool
| T_Test : ∀ t1 t2 t3 T Gamma,
Gamma ⊢ t1 ∈ Bool →
Gamma ⊢ t2 ∈ T →
Gamma ⊢ t3 ∈ T →
Gamma ⊢ test t1 t2 t3 ∈ T
where "Gamma '⊢' t '∈' T" := (has_type Gamma t T).
试试证明一个符合上面类型规则的东西吧～～
Example:
empty ⊢ (\x: Bool→Bool. (\y: Bool → Bool. (\z: Bool. y x z)))有类型
形式化的有
Example typing_example_3 :
∃ T,
empty ⊢
(abs x (Arrow Bool Bool)
(abs y (Arrow Bool Bool)
(abs z Bool
(app (var y) (app (var x) (var z)))))) ∈
T.
Proof:
根据直觉可以猜测存在类型T为(Bool -> Bool) -> (Bool -> Bool) -> Bool -> Bool.
形式化的有
(Arrow (Arrow Bool Bool) (Arrow (Arrow Bool Bool) (Arrow Bool Bool)))
根据T_Abs，如果要这个项目有类型，那么T11为(Bool->Bool),此时要有(x ⊢> (Bool -> Bool)) ⊢ t12 ∈ T12,此时再应用T_Abs,goal 变为(x ⊢> (Bool -> Bool)； y ⊢> (Bool -> Bool)) ⊢ t12 ∈ T12.
应用T_Abs,goal 变为(x ⊢> (Bool -> Bool)； y ⊢> (Bool -> Bool); z ⊢> Bool ) ⊢ t12 ∈ T12,之后再T_App两次，T_Var两次可以得到。
网友评论