1

I believe such terms are syntactically legal in (untyped) lambda calculus (see below), but the motivation for including them is not very clear to this newbie (e.g. because MN has no potential for reducibility). Perhaps I am hung up on the fact that while computation is about reduction, we are permitted to introduce irreducible expressions. I see that MN might reduce in a broader context, e.g. $(\lambda x. PMN)$. Perhaps this is why it is permitted. I guess this freedom is not necessary (?) but adds some additional expressive power?

For reference, recall that the class of $\lambda$-terms is defined inductively as follows:

  1. Every variable is a $\lambda$-term
  2. If M and N are $\lambda$-terms, then so is (MN)
  3. If M is a $\lambda$-term and x is a variable, then $\lambda x.M$ is a $\lambda$-term.
JRC
  • 516
  • I'm not sure I understand the question. Could you give me a concrete example of what you mean by an irreducible term? Note that reduction is a process applied on closed (and well-scoped) terms. – frabala Dec 31 '20 at 13:22
  • I suppose the OP means application terms which are not redexes, such as $x(\lambda y.y)$. – Natalie Clarius Dec 31 '20 at 13:26
  • It makes no sense, though, to reduce expressions that have free variables. In general, evaluation applies on closed and well-scoped expressions. I'm just repeating myself, I know... – frabala Dec 31 '20 at 16:27
  • 1
    @frabala Yes reduction is a process applied on closed (and well-scoped) terms. But in the example of lemontree is legal, but does not reduce. So I want a better understanding of the computational motivation for permitting such expressions. – JRC Dec 31 '20 at 18:24
  • Seems that it gives the untyped calculus more expressivity than typed calculus. – JRC Jan 01 '21 at 11:15
  • 1
    Reduction is not permitted on open expressions. Such expressions have no meaning. I can't see a computational motivation, but a syntactical one: how else can you construct the well-scoped term $\lambda x. x (\lambda y. y)$, if not by allowing the application $x (\lambda y. y)$ over which you later abstract? Btw, the open expression $x (\lambda y : T. y)$ is also allowed in the typed calculus. – frabala Jan 01 '21 at 12:19
  • When I first saw your question, I had written an answer that compares the untyped calculus with the simply typed calculus, thinking that your question regarded typing. I'll undelete my answer, though I'm not sure any more that your question has to do with that. Anyway, perhaps I really don't grasp the essence of your question. – frabala Jan 01 '21 at 12:21
  • 1
    @frabala - What do you mean by well-scoped term? – Taroccoesbrocco Jan 02 '21 at 06:32

1 Answers1

1

In the untyped $\lambda$-calculus, one can indeed write "meaningless" terms. Such terms include the application of a non-function to an argument and the application of a function to an argument over which the function is not defined. When attempting to evaluate such terms, you end up getting stuck at a point where you have reached an expression that is not yet in normal form, but can neither be further reduced. (After our discussion in the comments, I have to add that I consider reduction only over well-scoped terms, since it makes no sense to reduce open terms that have no meaning.)

I don't think historically there was motivation for allowing such terms. On the contrary, after the untyped $\lambda$-calculus, came the simply typed $\lambda$-calculus (STLC) that disallows such meaningless terms, but on the other hand it can be too restrictive. For example, the fixed-point combinator $\lambda f.(\lambda x. f\,(\lambda y. x\,x\,y))\,(\lambda x. f\,(\lambda y. x\,x\,y))$ that allows general recursion in the untyped $\lambda$-calculus, is no longer an acceptable term in a typed $\lambda$-calculus. In order to gain back recursion, you need to add it as a language primitive with new typing and evaluation rules for it (or use other techniques).

Another problem that simple types introduce is more practical rather than theoretical and involves code modularity. When coding, usually you want a single concept to be coded in a single place. This is not always possible in STLC (but is possible in System F, which is a more advanced typed calculus). Take for example the identity function $(\lambda x. x)$. In the untyped setting, you can assign this function to a variable named, say, "id" and then you can use id on any argument. In STLC, on the other hand, you would have to define separate "id" functions for applying them on integers or on booleans. These variations of "id" would only differ in type annotations and nowhere else: $(\lambda x : Int. x)$ and $(\lambda x : Bool. x)$. The "id" example is a very simple one, but things can get pretty messy for a bit more complex functions.

So altogether, I'd say there is no motivation to allow meaningless terms, but by disallowing them, you end up loosing more than what you wanted to get rid of. However, there are ways to gain back the extra losses, but then your language becomes more complex.

frabala
  • 3,732
  • Thanks very much for your help. – JRC Jan 04 '21 at 11:17
  • I agree with Taroccoesbrocco that it would be nice to define "well-scoped term" to avoid confusion. – JRC Jan 05 '21 at 08:51
  • 1
    I'm sorry for the confusion. I was a bit confused too when trying to answer this question... By well-scoped expression I only mean closed expression. It was a redundancy from my side, to use two terms for the same notion. – frabala Jan 06 '21 at 12:46