1

In untyped lambda calculus, if we define (as is common) the set $\Lambda$ of all $\lambda$-terms with:

\begin{align} &(1) & \text{if } u \in V, \text{then } u \in \Lambda \\ &(2) & \text{if } M \text{ and } N \in V, \text{then } (MN) \in \Lambda \\ &(3) & \text{if } u \in V \text{ and } M \in \Lambda, \text{then } (\lambda.u M) \in \Lambda \\ \end{align}

or in short using a grammar $$ \Lambda = V | (V.\Lambda) | (\Lambda \Lambda),$$

can we then prove that all $\lambda$-terms are 'finite'?

I ask because I have never seen talk about this in my books, so is it maybe due to the informal definitions? or because it forces to add more mathematics than wanted into the book in order to be able to create such a proof? or because this is not the topic for introductory books? or for some other reason?

jadn
  • 459
  • 1
    Finiteness of $\lambda$-terms is not a consequence of the rules you quoted. It is assumed in addition to them. – Fabio Somenzi Aug 09 '17 at 21:43
  • Isn't this only true if we are defining them 'inside' set theory? Is there not some way of defining them as finite discrete tree structures? The 'grammar' definition per example, does not that imply finiteness? – jadn Aug 09 '17 at 22:03
  • More than the grammar implying finiteness, it's the fact that formulae are usually taken to be finite sequences of symbols. It's so common, that if is often taken for granted. – Fabio Somenzi Aug 09 '17 at 22:11
  • All (1)-(3) really state is a closure condition, not minimality. If that's stated, then they're all finite, but using only the above postulates there may be "non-standard" lambda terms. – Malice Vidrine Aug 10 '17 at 00:49

2 Answers2

2

If $\Lambda$ is just some set which satisfies (1), (2), and (3), then "infinite" terms are not precluded. However, such definitions are intended to be inductive definitions which is the "additional assumption" Fabio Somenzi mentions. There are a variety of ways to formalize "inductive": initial algebras, least fixed points, minimality. In a set-theoretic context, the last is usually used. That is, we say for all sets $S$ which satisfy (1), (2), and (3), $\Lambda\subseteq S$ which is to say, $\Lambda$ is assumed to be the smallest set satisfying those constraints. It's clear a suitable set of finite terms is closed under rules (2) and (3) (and trivially for (1)) so $\Lambda$ doesn't include any infinite terms.

Derek Elkins left SE
  • 24,967
  • 1
    Without the minimality condition present, how would one prove that there is a non-finite element? – jadn Aug 10 '17 at 05:18
  • 2
    The minimality condition picks out a unique solution, namely $\Lambda$. Without it, $\Lambda$ is still a possible solution so you can't prove that there is an infinite term, but you can also no longer assume every term is finite. In particular, without the minimality condition, you can't do induction. To guarantee the existence of an infinite term requires additional assumptions. – Derek Elkins left SE Aug 10 '17 at 08:13
0

It's entirely possible to have infinite terms conforming to the syntax you stated. An important class of such terms are the Rational Infinite terms. They are given by the property that, though they may be infinite, they have only a finite number of distinct subterms. For instance, $D_3 D_3$ can be thought of as having the rational infinite lambda term $⋯ D_3 D_3 D_3 D_3$ as its normal form, where $D_3 = λx·x x x$. In particular, the combinator reduction engine Combo, when given $D_3 D_3$ will recognize it as a "cyclic term", recognizing that it's contained as a subterm in its own reduction as $D_3 D_3 → ⋯ → D_3 D_3 D_3$ and stop reduction. It's entirely possible to modify "Combo" so that (a) it will actually produce the rational term as a normal form, rather than blocking reduction, and (b) it can process rational infinite lambda terms. I just never got around to making the upgrade (yet).

A finite syntax for rational infinite terms requires a way to explicitly refer to embedded subterms, since the term-subterm relation may be cyclic. So, the natural and obvious extension to the syntax is to add more clauses $Λ → X : Λ$, for labeled subterms containing one main term, and $Λ → \text{goto} X$ for a reference to a labeled subterm. Then the normal form of $D_3 D_3$ will just be $X: (\text{goto} X) D_3$. On top of this, you can graft the other control-flow structure of imperative programming languages, because a rational infinite lambda term is, itself, just an imperative control-flow structure in disguise.

Edit: (Search, search, ding) Bibliography time!

Lukasz Czajka, A New Coinductive Confluence Proof For Infinitary Lambda Calculus (PDF)
Jörg Endrullis and Andrew Polonsky, Infinitary Rewriting Coinductively (PDF)
J. R. Kennaway, J. W. Klop, M. R. Sleep, F. J. de Vries, Infinitary lambda calculus, Theoretical Computer Science, 175 (1), 1997-03-30, 93-125.

NinjaDarth
  • 540
  • 2
  • 4