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?
相关问题
- Generating powerset in one function, no explicit r
- Forming Lisp code to task — related to flatten lis
- Beta reduction in lambda calculus: Order of evalua
- unfold function in scheme
- Confused by Lisp Quoting
相关文章
- Does learning one Lisp help in learning the other?
- What is the definition of “natural recursion”?
- How do I write a macro-defining macro in common li
- How can I unintern a qualified method?
- Changing the nth element of a list
- sleep in emacs lisp
- comma-comma-at in Common Lisp
- Sending HTTP POST in Racket
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.
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:
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.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.