What type of lambda calculus would Lisp loosely be

问题:

I'm trying to get a better grip on how types come into play in lambda calculus. Admittedly, a lot of the type theory stuff is over my head. Lisp is a dynamically typed language, would that roughly correspond to untyped lambda calculus? Or is there some kind of "dynamically typed lambda calculus" that I'm unaware of?

回答1:

Lisp is a dynamically typed language, would that roughly correspond to untyped lambda calculus?

Yes, but only roughly. In the "pure" untyped lambda calculus, everything is coded as functions. (You can google for the popular "Church encoding" and the less popular "Scott encoding".) Lisp has non-functional data, like atoms and numbers and such, so this would count as "untyped lambda calculus extended with constants."

Another important difference is in order of evaluation. Rules for reducing lambda-calculus terms are highly nondeterministic. (There's a theorem, the Church-Rosser theorem, which says loosely that as long as things terminate, order of evaluation doesn't matter.) In practice lambda terms are typically reduced using leftmost-outermost aka "normal-order" reduction because if any reduction strategy terminates, that one does. This is very different from Lisp which always evaluates arguments to normal form before doing a beta-reduction. This evaluation order is called "call by value."

In summary, Lisp corresponds to an untyped, call-by-value lambda calculus extended with constants.

回答2:

John McCarthy introduced LISP in his April, 1960 paper "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I". The following paragraph is from page 6:

e. Functions and Forms. It is usual in mathematics — outside of mathematical logic — to use the word “function” imprecisely and to apply it to forms such as y² + x. Because we shall later compute with expressions for functions, we need a distinction between functions and forms and a notation for express- ing this distinction. This distinction and a notation for describing it, from which we deviate trivially, is given by Church [3].
...
3. A. CHURCH, The Calculi of Lambda-Conversion (Princeton University Press, Princeton, N. J., 1941).

The Wikipedia article on lambda-calculus has a history of Church's publications. The 1941 paper referenced by McCarthy seems to be about the typed lambda-calculus, in contradiction to the Wikipedia article's introduction.

The lambda keyword in Lisp can be understood to refer to the lambda-calculus only through analogy. A Lisp lambda expression is a type of anonymous function.

回答3:

Lisp is not 'a lambda calculus', I don't know what 'a lambda calculus' is.

If you want to identify lambda calculi by there type system then Lisp is its own of course. The 'lambda' keyword in any lisp before Scheme is certainly pretentious, and after Scheme there's room too to say it is. Just using 'func' would have been more humble. Lisp is a list processor mainly, not a 'lambda calculus'

I also wrote a rather extensive article about this once that attempts to demonstrate why A: the term 'functional programming' is meaningless and B: why the speaking of 'a lambda calculus' rather than 'a type system' is so too:

http://blog.nihilarchitect.net/archives/289/on-functional-programming/

Also, keep in mind that in Lisp, all functions are in effect single argument and can only be have lists as their arguments.