对于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两次可以得到。
网友评论