你好,类型(六):Simply typed lambda calculus


简单类型化演算(simply typed lambda calculus)

是无类型演算的类型化版本,

它是众多类型化演算中最简单的一个。


它只包含一个类型构造器(type constructor)

即,接受两个类型作为参数,返回一个函数类型


下文中,我们首先从最基础的概念说起,

详细的区分项(term)和值(value)的概念,

然后介绍简单类型化演算系统的求值规则和类型规则。


1. 项和值



1.1 项

项(term)是一个语法概念,一个合法的项,指的是一段符合语法的字符串。例如,

系统中,项的定义如下,


它表明,一个合法的项,要么是一个变量

要么是一个抽象(abstraction)

要么是一个应用(application)


1.2 值

值(value)是一个和语义相关的概念,有三种常用的方法为项指定语义。

(1)操作语义,通过定义一个简单的抽象机器,来说明一个程序语言的行为。

(2)指称语义,一个项的语义是一个数学对象。

(3)公理语义,不是首先定义程序的行为,而是用项所满足的规则限定它的语义。


下面我们采用操作语义的方法,来定义求值的概念。

首先,我们人为指定项的一个子集,将其中的元素称为值。


假如项的定义如下,

我们可以定义值,

值可能是项被求值的最终结果,但也不全是,因为对某些项的求值过程可能不会终止。


1.3 求值规则

求值规则,是定义在项上的推导规则,例如,

(1)

(2)

(3)

其中,表示,项可以一步求值为项


1.4 范式

一个不含自由变量的项,称为封闭项,封闭项也称为组合子。

例如,恒等函数就是一个封闭项。


如果没有求值规则可用于项,就称该项是一个范式。

范式可能是一个值,也可能不是,但每一个值都应该是范式。


如果一个封闭项是一个范式,但不是一个值,就称该项受阻。

不是值的范式,在运行时间错误分析中起着极其重要的作用。


2. 类型



2.1 类型上下文

一个类型上下文(也称类型环境),是一个变量和类型之间绑定关系的集合。

空上下文,可以记为,但是我们经常省略它。


用逗号可以在右边加入一个新的绑定,例如,

,表示项在空的类型上下文中,有类型


2.1 类型规则

是一个新的系统,比起而言,

增加了一些基于类型的推导规则。


其中,项的语法如下:

(1)

(2)

(3)


推导规则:

(1)

(2)

(3)


根据以上的推导规则,我们可以证明,


2.3 求值规则

系统中,值的定义如下:

(1)


求值规则,定义如下:

(1)

(2)

(3)


其中(2),相当于变换,

,表示将中所有自由出现的换为


2.4 Curry-style and Church-style

对于系统来说,通常有两种不同风格的解释方式,

如果我们首先定义项,然后定义项的求值规则——语义,

最后再定义一个类型系统,用以排除掉我们不需要的项,

这种语义先于类型的定义方式,称为Curry-style。


另一方面,如果我们定义项,然后再给出良类型的定义,

最后再给出这些良类型项的语义,就称为Church-style,类型先于语义,

在Church-style的系统中,我们不关心不良类型项的语义。


历史上,隐式类型的演算系统,通常是Curry-style的,

而显式类型的演算系统,通常是Church-style的。


3. 关于单位类型

简单类型化演算,直接用起来可能并不好用,

人们会再为它扩充一些类型,例如,添加一些基本类型或者

定义单位类型,列表类型,元组类型,和类型,等等。


下面我们选择单位类型进行介绍。


满足单位类型的项只有一个,为此我们新增一个项的定义,


再新增一个类型的定义,


以及一个推导规则,


的作用类似于C和Java中的类型,主要用于表示副作用,

在这样的语言中,我们往往并不关心表达式的结果,而只关心它的副作用,

因此,用来表示结果的类型,是一个合适的选择。


这里提到单位类型,是为以后Top类型和Bot类型做铺垫。


参考

Wikipedia: Simply typed lambda calculus

类型和程序设计语言