评估形式化语义的三种方法是什么？
评估形式化的语义，就是评估项term的语义，
主要有：
操作语义（将语言视为抽象的自动机）
指称语义（定义一集数学的对象domains，并且定义一个解释函数，将terms映射到domains实体中）
公理化语义（公理化语义从定义的自身出发推导出语言的含义）
one-step evaluation relation：
满足规则的最小二进制关系
什么是mutable reference cells 和 nonlocal exception handling？
类型系统是指一种根据计算出的值的种类对于词语进行分类，从而证明某程序行为不会发生的可行语法手段。
给定语言中能够使用类型系统消除的错误一般称为运行时类型错误runtime type error，一般的类型系统相对直接的检查能够校验简单的类型错误和数组越界。
一个类型安全的语言是编程时不会危害到自身的语言，是一个保护其抽象的语言，
语言安全性可以由运行时或静态类型检查保证，Scheme没有静态检查，但是仍然类型安全。如果建立了动态检查的设施，那么检查的代价将会很小（但是也存在一些Basic方言 提供底层原语，因此不安全）
不安全的语言通常提供效果最佳的静态类型检查器，但是一般不能够保证良类型的程序是良行为的
在对象变量上取值的变量称为元变量，不含自由变量的项称为封闭项，封闭项也称为组合子，最简单的组合子称为恒等函数 id = lambdax（x）只输出其变元。 不动点组合式可以用来定义递归函数
full beta规约：任何时候可以以任意顺序规约 规范顺序
normal order策略：最左侧最外面先被规约
按名调用call by name：不针对抽象进行规约。
haskell采用按需规约call by need的方式
一般则采用call by value的方式
使用lambda项表示的数称之为church数值 Church 编码是一种“抽象方法”，它将“数字”、“运算”等概念全数“抽象”成λ- 演算
简单代换一个项x到t，使自由变量编程收到限制的变量的情况称为变量捕捉
纯lambda演算是图灵完备的，为了解决结果的发散问题，有两种方案，第一种使用项的类型注释来显式检查类型的结果，第二种是使用类型检查器自己推导或者重构这个信息。
curry-howard对应：一个命题P的证明是由P的具体证据组成的