简单类型化演算（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类型做铺垫。