我觉得你对这些问题很有自己的想法

所以没人干预你的想法

那是过程式
才有 assign，赋值的概念

type checking 里 assign 则是 指派 的意思

lisp-1和lisp-2只是一个遗留的历史概念，何必追究呢，

不如去研究一下 Haskell 的 Hindley-Milner 多态类型系统？

HM 的 type inference 是纯 unification 的

没入门
告辞

那为什么不去研究下system F。。。

没入门

既然简单，我就不会叫 System F 这种晦涩的名字

多态系统可以解决，谁说 a 必须只能指代 函数a 或 量a 其中之一的？

JW 你跟我 brief 一下 Lambda 演算的基本 term 和 operation

不会

要不然我不清楚你说得到底是有引用背书的，还是你自己造的

没听说过草

还有term一说吗

指定理？

我都会自己造词了吗。。。

Lambda 演算是基于项(term) 的形式化系统，为什么没有 term？

Lambda calculus 代表的是一个语言的抽象方式（包括作用域）
以及求值的模式（beta-reducation 操作）

Lambda 演算本身不是完整的（准确的说应该是严重可扩展），但即便这样它也可以基于具名抽象引用自己的基元操作，构造新行为

Lambda 演算只有三种基本项，
Abstraction: λarg. body
上面我用的是 currying 的形式，多参函数可以变成许多单参函数
Application: (f x)
Variable: x
就是包含在 lexical scope 里的 name binding