10 ms·

The Lambda Calculus

177 points by infinity 14y ago

rhcpfan1 14y ago
You can see where the name 'Y Combinator' came from. Thanks.
- elliott99 14y ago
  can you explain this?
  - igravious 14y ago
    Go to the page and search for "Curry's paradoxical combinator" See also: http://en.wikipedia.org/wiki/Fixed-point_combinator#Y_combinator http://en.wikipedia.org/wiki/Fixed-point_combinator#Y_combin...
hsmyers 14y ago
Very nice article. The HTML version is free, the .pdf version which will be available after the 21st will cost you $10 a year---all things considered, a useful service at a very reasonable cost.
- p4bl0 14y ago
  Very nice introduction indeed. But there are tons of good introduction to the lambda-calculus available for free in any languages that have a computer science degree taught in. And a lot of them goes into a lot more details in particular on typed lambda-calculi.
  - kenko 14y ago
    <a href="http://plato.stanford.edu/entries/type-theory/>Did http://plato.stanford.edu/entries/type-theory/>Did someone say type theory</a>? That $10 also gets you nice pdfs of some really excellent articles on a very large range of philosophical topics (I mean it is the SEP, after all). A worthwhile use of ten bucks, IMO. (I used to work for Zalta, but I'd have and express the same high opinion of the SEP regardless.)
sb 14y ago
Nice article (the Stanford Encyclopedia of Philosophy has many more, btw.), but I like the "Introduction to Lambda Calculus" by Henk Barendregt (one of the people working in Lambda calculus, see for instance the citation to his book "The Lambda Calculus: Its syntax and semantics." in the references), which has the added benefit of being free: http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex... (also covers typed lambda calculus AFAIR)
- dajohnson89 14y ago
  I second the recommendation of SEOP. It treats a wide array of topics with surprising depth and rigor.
why-el 14y ago
Does anybody know whether this is a good introduction for someone who plans to go over the Lambda Papers in detail in about two weeks?
- mahmud 14y ago
  The it will be a more than adequate preparation. In fact, it just might be overkill :-) But read it nevertheles. Plenty of materials out there, it might help you to learn a Lisp dialect, Scheme is excellent and closest to the lambda calculus.
knowtheory 14y ago
The Lambda Calculus is more widely applicable than most people know too. One of the dominant modeling paradigms in formal semantics (e.g. understanding the meaning of human language) is built around a typed lambda calculus called Montague Semantics (see http://plato.stanford.edu/entries/montague-semantics/ http://plato.stanford.edu/entries/montague-semantics/ )
- adimitrov 14y ago
  Montague Semantics is really interesting — and totally inadequate! Still, it's a very good approach, and all formal systems for natural language semantics we know of today are still totally inadequate. It's proving to be very difficult to model natural languages as formal languages. The basic idea of MG (and CCG) is to treat lexical items ("words") as function in the lambda calculus, and use higher order functions to compose these lexical functions, yielding truth conditions in a logical language (typically anything from predicate logic, over intensional or two-sorted type logic, to even higher order logic, dynamic logic, probabilistic logic, etc.) Some of the more interesting extensions of traditional MG are introduced by Combinatorial Categorial Grammar, which, you guessed it, uses combinators to enable compositional analyses of lexical items even in complex syntactic constructions. One more thing that is very interesting is that continuation passing style transformations on these combinators and lexical functions seems to be rather effective! Read Barker 2004 for an overview. It's a very interesting field of study, but almost entirely academic. There is very little commercial interest nowadays, as everybody is all about statistical NLP.
  - knowtheory 14y ago
    Absolutely, it is inadequate for modeling language, but then everything is! (My assertion is that so much contextual information is required to converse with humans that one needs to build a proper AI in order to have unrestricted conversation. That or you have to reliably constrain conversation to a domain) The importance of systems like Montague Semantics are to kind of scope out what sort of thing we need to be able to model language in the abstract. Statistical NLP is definitely way better for building engineering systems that are deployed to accomplish particular tasks.
evincarofautumn 14y ago
If Church numerals’ unary representation bothers you, there is an efficient embedding of naturals in λ-calculus as linked lists of Booleans. Well, more efficient than the alternative… http://useless-factor.blogspot.com/2007/04/thoughts-on-church-numerals.html http://useless-factor.blogspot.com/2007/04/thoughts-on-churc...
jacquesm 14y ago
If this stuff interests you have a look at Matt Might's blog, it's full of interesting goodies and extremely accessible. For example: http://matt.might.net/articles/compiling-up-to-lambda-calculus/ http://matt.might.net/articles/compiling-up-to-lambda-calcul...
tekniiq 14y ago
what perent of programmers actually even use the lambda calculus?
- fragsworth 14y ago
  Directly? Not many... Indirectly, because their language supports features that came about as a result of this? Almost everyone. It's kind of like asking what percentage of programmers use binary arithmetic.
- mahmud 14y ago
  100%. The lambda calculus forms the backbone of most theories of programming languages. Functional programmers use enriched forms of it directly, but all others, at least the useful ones, do make use of lambda-calculus techniques. The LC demarcates the border between high and low-level languages. High-level programming languages have reducible expressions, low-level ones are flat. HLPLs have notion of heirarchical variable scope, within which some variables are "bound" while others are "free" and escape to a parent environment; while LLPLs often have a flat dictionary of variables, if at all. The lambda-calculus can also be higher-level than mainstream languages. Most PLs treat functions with identical bodies as different, due to name/pointer inequality. In the LC, two forms are equal if they reduce to the same basic form, and names of bound variables are insignificant.
  - warfangle 14y ago
    Any sufficiently advanced C program has redefined LISP poorly; any sufficiently advanced LISP program has redefined C poorly. I can't recall where I first read this conjecture (booze; mobile).
    - mahmud 14y ago
      You butchered Greenspun's Tenth Rule (booze; dekstop) http://en.wikipedia.org/wiki/Greenspun%27s_tenth_rule http://en.wikipedia.org/wiki/Greenspun%27s_tenth_rule
      - 14y ago
mahmud 14y ago
The Stanford Encyclopedia of Philosophy, one of my favorite hangouts on the net for the last decade. Enjoy it.
joe_the_user 14y ago
Wow, I had never noticed how intension, used here in "intensional definition", was a different word than intention. I wonder what percentage of people who looked at this stuff outside a formal classroom haven't been confused by this? http://en.wikipedia.org/wiki/Intensional_definition http://en.wikipedia.org/wiki/Intensional_definition
cerebrum 14y ago
nice
sdee 14y ago
ultimate….deccansojourn.com

The Lambda Calculus

177 points by infinity 14y ago

rhcpfan1 14y ago

You can see where the name 'Y Combinator' came from. Thanks.

elliott99 14y ago
can you explain this?
- igravious 14y ago
  Go to the page and search for "Curry's paradoxical combinator" See also: http://en.wikipedia.org/wiki/Fixed-point_combinator#Y_combinator http://en.wikipedia.org/wiki/Fixed-point_combinator#Y_combin...

hsmyers 14y ago

Very nice article. The HTML version is free, the .pdf version which will be available after the 21st will cost you $10 a year---all things considered, a useful service at a very reasonable cost.

p4bl0 14y ago
Very nice introduction indeed. But there are tons of good introduction to the lambda-calculus available for free in any languages that have a computer science degree taught in. And a lot of them goes into a lot more details in particular on typed lambda-calculi.
- kenko 14y ago
  <a href="http://plato.stanford.edu/entries/type-theory/>Did http://plato.stanford.edu/entries/type-theory/>Did someone say type theory</a>? That $10 also gets you nice pdfs of some really excellent articles on a very large range of philosophical topics (I mean it is the SEP, after all). A worthwhile use of ten bucks, IMO. (I used to work for Zalta, but I'd have and express the same high opinion of the SEP regardless.)

sb 14y ago

Nice article (the Stanford Encyclopedia of Philosophy has many more, btw.), but I like the "Introduction to Lambda Calculus" by Henk Barendregt (one of the people working in Lambda calculus, see for instance the citation to his book "The Lambda Calculus: Its syntax and semantics." in the references), which has the added benefit of being free: http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex... (also covers typed lambda calculus AFAIR)

dajohnson89 14y ago
I second the recommendation of SEOP. It treats a wide array of topics with surprising depth and rigor.

why-el 14y ago

Does anybody know whether this is a good introduction for someone who plans to go over the Lambda Papers in detail in about two weeks?

mahmud 14y ago
The it will be a more than adequate preparation. In fact, it just might be overkill :-) But read it nevertheles. Plenty of materials out there, it might help you to learn a Lisp dialect, Scheme is excellent and closest to the lambda calculus.

knowtheory 14y ago

The Lambda Calculus is more widely applicable than most people know too. One of the dominant modeling paradigms in formal semantics (e.g. understanding the meaning of human language) is built around a typed lambda calculus called Montague Semantics (see http://plato.stanford.edu/entries/montague-semantics/ http://plato.stanford.edu/entries/montague-semantics/ )

adimitrov 14y ago
Montague Semantics is really interesting — and totally inadequate! Still, it's a very good approach, and all formal systems for natural language semantics we know of today are still totally inadequate. It's proving to be very difficult to model natural languages as formal languages. The basic idea of MG (and CCG) is to treat lexical items ("words") as function in the lambda calculus, and use higher order functions to compose these lexical functions, yielding truth conditions in a logical language (typically anything from predicate logic, over intensional or two-sorted type logic, to even higher order logic, dynamic logic, probabilistic logic, etc.) Some of the more interesting extensions of traditional MG are introduced by Combinatorial Categorial Grammar, which, you guessed it, uses combinators to enable compositional analyses of lexical items even in complex syntactic constructions. One more thing that is very interesting is that continuation passing style transformations on these combinators and lexical functions seems to be rather effective! Read Barker 2004 for an overview. It's a very interesting field of study, but almost entirely academic. There is very little commercial interest nowadays, as everybody is all about statistical NLP.
- knowtheory 14y ago
  Absolutely, it is inadequate for modeling language, but then everything is! (My assertion is that so much contextual information is required to converse with humans that one needs to build a proper AI in order to have unrestricted conversation. That or you have to reliably constrain conversation to a domain) The importance of systems like Montague Semantics are to kind of scope out what sort of thing we need to be able to model language in the abstract. Statistical NLP is definitely way better for building engineering systems that are deployed to accomplish particular tasks.

evincarofautumn 14y ago

If Church numerals’ unary representation bothers you, there is an efficient embedding of naturals in λ-calculus as linked lists of Booleans. Well, more efficient than the alternative… http://useless-factor.blogspot.com/2007/04/thoughts-on-church-numerals.html http://useless-factor.blogspot.com/2007/04/thoughts-on-churc...

jacquesm 14y ago

If this stuff interests you have a look at Matt Might's blog, it's full of interesting goodies and extremely accessible. For example: http://matt.might.net/articles/compiling-up-to-lambda-calculus/ http://matt.might.net/articles/compiling-up-to-lambda-calcul...

tekniiq 14y ago

what perent of programmers actually even use the lambda calculus?

fragsworth 14y ago
Directly? Not many... Indirectly, because their language supports features that came about as a result of this? Almost everyone. It's kind of like asking what percentage of programmers use binary arithmetic.
mahmud 14y ago
100%. The lambda calculus forms the backbone of most theories of programming languages. Functional programmers use enriched forms of it directly, but all others, at least the useful ones, do make use of lambda-calculus techniques. The LC demarcates the border between high and low-level languages. High-level programming languages have reducible expressions, low-level ones are flat. HLPLs have notion of heirarchical variable scope, within which some variables are "bound" while others are "free" and escape to a parent environment; while LLPLs often have a flat dictionary of variables, if at all. The lambda-calculus can also be higher-level than mainstream languages. Most PLs treat functions with identical bodies as different, due to name/pointer inequality. In the LC, two forms are equal if they reduce to the same basic form, and names of bound variables are insignificant.
- warfangle 14y ago
  Any sufficiently advanced C program has redefined LISP poorly; any sufficiently advanced LISP program has redefined C poorly. I can't recall where I first read this conjecture (booze; mobile).
  - mahmud 14y ago
    You butchered Greenspun's Tenth Rule (booze; dekstop) http://en.wikipedia.org/wiki/Greenspun%27s_tenth_rule http://en.wikipedia.org/wiki/Greenspun%27s_tenth_rule
    - 14y ago

mahmud 14y ago

The Stanford Encyclopedia of Philosophy, one of my favorite hangouts on the net for the last decade. Enjoy it.

joe_the_user 14y ago

Wow, I had never noticed how intension, used here in "intensional definition", was a different word than intention. I wonder what percentage of people who looked at this stuff outside a formal classroom haven't been confused by this? http://en.wikipedia.org/wiki/Intensional_definition http://en.wikipedia.org/wiki/Intensional_definition

cerebrum 14y ago

nice

sdee 14y ago

ultimate….deccansojourn.com