lambda calculus最早是在1930年代被Alonzo Church 提出，可是因为罗素悖论所以被证实是一个inconsistent的系统，所以在1940年Church又提出了simply typed lambda calculus。
而Lisp是在1958年被John Macarthy所设计的。既然已经知道原本的untyped lambda calculus有所缺陷，为何当初还要依据这个理论设计呢？比较现代的语言也都是改用typed lambda calculus为基础(ML, Haskell)，是不是能说明现代PLT学界普遍认为typed lambda calculus其实是个比最初untyped lambda calculus更well-designed的设计呢？
大概lisp最开始就没想着lambda演算吧
Lisp根本不是untyped lambda calculus，Lisp是具名的（比如：define），而lambda calculus是匿名的。
匿名的坏处就是你无法通过名字来引用自身 —— 无法递归。
untyped lambda calculus是图灵完全的（有Y组合子，并且只能用Y组合子或类似技术来实现递归）。
typed lambda calculus不是图灵完全的（没有Y组合子，如果你使用具名的方法来实现递归，那就不是typed lambda calculus）
图灵完全一般被认为是语言强大的象征，所以不能说untyped lambda calculus 不如 typed lambda calculus。
但这些和Lisp没什么关系，因为Lisp是具名的，它根本不是untyped lambda calculus。
同理 Haskell 也不是 typed lambda calculus。
lz问基于与否，不是问是不是。
真正硬核的lambda calculus，写个循环都要写Y combinator的那种就太原始了。
感谢回答。
我并没有说Lisp就是untpyed lambda calculus，或是Haskell就是typed lambda calculus，我的意思是这两种语言是分别基于这两种不同的理论基础所建构出来的。
这句话部份认同。我并不认为图灵完全就是强大的象征。在图灵机之前lambda calculus便存在，我想当初设计这些理论是为了有一个正规严谨的系统进行逻辑推理，不能单以计算系统的强弱就断定谁好谁坏。
但我个人也不认为untyped lambda calculus就是比较先进的理论，他虽然绕过了paradox，但是那些奇奇怪怪的悖论很多其实是集合论自己对于Universe定义上的瑕疵（个人的浅见，参考就好）
simply typed lambda calculus 确实是一个 consistent 系统，但这不代表ML、Haskell 也是 consistent 系统。
ML Haskell 也是不一致的，因为他们是具名的、可以引用自身，这一点和 Lisp 没区别。
untyped lambda calculus 相比 typed lambda calculus 确实有劣势（inconsistent），但也有优势（turing complete）。
如果你把 Lisp 看成 untyped lambda calculus，Haskell、ML看成 typed lambda calculus，但由于具名的关系，以上的劣势和优势相当于都被移除了，最后大家都是图灵完全的。
接下来的问题就是，Lisp是动态类型语言，Haskell、ML是静态类型语言，它们哪个好的问题。。。
只是John 选择了动态语言，这或许和当年computer algebra 和 symbolic computation 比较火有关，也可能和s-exp的美学有关。。。
Turing incompleteness 只限于 simple typed lambda，比如在一个有 T 作为所有类型的 supertype 的支持 subtype 的类型系统完全是可行的。即 untyped = unityped
当然就放现在也没能力做一个这样的系统。
然后 Turing completeness 最直观的体现就是 subtyping, polymorphism, message passing
想知道为什么具名的话就不是consistent的？希望可以多讲解一点，或是指引一些文章阅读。
有点概念了。其实我不是想讨论到底Lisp好还是Haskell好，也没有想要讨论动态或静态谁优谁劣。主要还是想知道typed vs untyped lambda calculus之间的优缺点。在typed lambda calculus的Wiki 上面查到了这句话，想拿出来讨论看看
From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus
but from another point of view, they can also be considered the more fundamental theory and untyped lambda
calculus a special case with only one type.
希望可以有大神解释一下怎么从不同角度看待typed vs untyped之间的差异以及优劣
这么说吧，大家都是编译成汇编的，不管动态类型静态类型本质上程序都是一样的，类型系统是用来辅助分析程序的，不管静态动态不影响一个完全正确并按照预期运行的实际程序，挑 simply typed lambda 是因为这个系统简单好分析，并不会给程序带来额外的特性，比如突然就能解决计算机不能解决的问题了。静态能帮助提前发现问题，也不见得能发现所有问题，动态则能保证出问题时的收尾，代价是程序的额外冗沉
没啥可解释的，就和看到 monad is just a monoid in the category of endofunctors 一头雾水后来明白 monad 是啥以后也找不到什么更好的描述了一样。
这篇并没有讲 untyped 和 typed 的区别。而是论证静态类型语言中用的动态特性和动态语言的静态分析以给出动态静态之争的结论。
这篇文章没有讲typed vs untyped lambda calculus，而是讲我们可以从 Church typist 和 Curry typist 这两种角度来看待 动态语言 和 静态语言，最后得出了一个结论：
Gradual Typing 才是未来方向（即：动态和静态语言的混合编程）。
对Gradual type没什么研究，不过这思路确实很诱人。。。
听说Typescript就是基于Gradual type？现在好像应用很广泛？（2018最火的语言？）
只是我还没用过Typescript，想听听你的看法 。
自己回答一下一开始我的问题。根据John Marcathy在1960年发的论文Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I ，里面引用的是Church 在1941年的论文，也就是simply lambda calculus那篇，所以Lisp的原形应该是参考了有类型的LC，只是最后设计成了动态语言。
因为具名的话就可以引用自己了，这样你就可以写出所谓“死循环”。
“死循环”从本质上讲就是你的程序企图接受一个不可判定的语言。从逻辑上看就是这个系统有矛盾，即：存在"无法证明真也无法证明假的命题"。所谓"无法证明真也无法证明假的命题" ，即：“如果你它是真的，则是假的，如果是假的，则它是真的”。这类似于罗素悖论里你向AI提问说 “理发师该不该为自己理发？”，AI进入loop
如果Haskell真的是 typed lambda calculus，则它们不应该让你引用自身从而让你写出任意的递归函数（注意：Haskell是没有Y组合子的，Y组合子只能出现在动态语言里）
感谢说明。另外关于typed lambda calculus有些疑惑的地方
如果从计算模型的角度出发，untyped LC是否是个比typed LC更强大的模型？这边让我困惑的是，虽然typed LC不是turing complete，可是他可以解决像是halting problem等问题，也就是说在计算能力上两者并不是某一方被包含于另一方，既然这样是怎么得出untyped LC比typed LC更强大的结论？
untyped LC可以被看成是typed LC的一种特例（只有一种类型的typed LC)，这是否意谓typed LC是个比untyped LC更基本的理论（有点像数学上function也是relation的其中一种）？但是如果从另一个角度看，typed LC 也可以看成是在原本的untyped LC上加入额外的限制（所以导致计算能力减弱），如果从这个角度出发，untyped LC就是比typed LC基本的理论。到底这两种理论谁才是更general, 更底层的计算模型呢？
A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program terminates. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be Turing complete.[1] That means that there are computable functions that cannot be defined in the simply typed lambda calculus (and similarly there are computable functions that cannot be computed in the calculus of constructions or System F). As an example, it is impossible to define a self-interpreter in any of the calculi cited above.[2][3]
The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.
typed LC加入额外限制保证safety，即任意的well-typed term都可以求值最终得到normal form，也就是well-typed的程序都会终止
是的。typed LC之所以“能解决halting problem”，只不过是因为它的计算能力低下。有很多untyped LC能解决的问题typed LC无法解决。
是的。但这里的typed和上面所讲的typed不是同一个概念。
因为我们通常讲typed LC是指的STLC，而这里讲的typed是更广意义上typed。
http://r6.ca/blog/20060919T084800Z.html
所以你完全没读就下了结论，JMC 只借用了 lambda notation，直到 Scheme 出现为止，Lisp 从来都不是 lambda calculus 的 model，早期的 Lisp 甚至没有考虑过 high order function。至于为什么是动态语言，因为最早的 Lisp 实现只有一种数据类型，就连数学运算都是靠 church encoding 做的，真正的 unitype 。后来的实现为了模拟这个特性自然就做了动态类型了。