What type of lambda calculus would Lisp loosely be an example of?

Question

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?

Answer 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.

Answer 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.