English 中文(简体)
What type of lambda calculus would Lisp loosely be an example of?
原标题:

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?

最佳回答

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.

问题回答

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 y2 + 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.





相关问题
Lisp code called from Java

Long story: I am doing a project for my functional programing class, and I thought of writing an AI controller in Lisp, for the Mario AI competition. I was looking over frameworks/libraries/ways of ...

Emacs, Zen-Coding mode, and Putty

I use emacs via Putty and since Putty doesn t send certain key combinations to the remote console I generally need to re-bind them to other key combinations. After installing the amazing Zen-Coding ...

In Which Cases Is Better To Use Clojure? [closed]

I develop in Lisp and in Scheme, but I was reading about Clojure and then I want to know, in which cases is better to use it than using Lisp or Scheme? Thanks

lambda-gtk negative pointer

I was trying to write my own put-pixel on (Gdk) pixbuf in Lisp. When I finally realized how I can operate on C pointers in CL, new obstacle came along - (gdk:pixbuf-get-pixels pb) returns me negative ...

Is there a common lisp package naming convention?

I have created some of my own user packages and have run into a name clash. In Java, the naming convention is to use your domain name in the package name: e.g. import com.example.somepackage;. Are ...

SOAP request from within an AutoLISP/AutoCAD macro

We have built a webservice for a client that uses AutoCAD. They have a macro that runs in AutoCAD that builds a SOAP request. But they have not figured out how to actually send() the soap request to ...

热门标签