21

No, it's not possible. Consider the following two inhabitants of the type $(A \to B) \to (A \to B)$. $$ \begin{array}{l} M = \lambda f.\;f \\ N = \lambda f.\;\lambda a.\; f\;a \end{array} $$ These are distinct $\beta$-normal forms, but cannot be distinguished by a lambda-term, since $N$ is an $\eta$-expansion of $M$, and $\eta$-expansion preserves ...


11

Another possible answer to Neel's perfectly correct one: Suppose that there is a combinator $E$, well-typed in system F such that the above condition holds. The type of $E$ is: $$ E : \forall \alpha.\alpha\rightarrow \alpha\rightarrow {\bf bool}$$ It turns out that there is a theorem for free that expresses that such a term is necessarily constant: $$ \...


9

The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of reductions, but clarify the presentation in my opinion. Let's assume your language is given by the following grammar. $$ \newcommand{\PROGRAM}[1]{\mathsf{#1}} ...


9

With general recursive types you can define the type type T = T -> T With that type you can type self-application -- and in fact, every term of the untyped lambda calculus, including any of the well-known fixed-point operators. For example, the Y operator: Y = \f:T. (\x:T. f (x x)) (\x:T. f (x x))


8

I'll summarize the comments from chi, and sketch the proof that There can be no proof of $\mathrm{False}:=\forall X:*.X$ in the CoC in head normal form. Furthermore, this fact can be proven in a weak theory, say Peano Arithmetic (though the excluded middle is not required). This fact implies that if the CoC is normalizing, then it is consistent, and ...


8

There's a bit of freedom in what we considre "the same value". Let me show that there is no such algorithm if "the same value" means "observationally equivalent". I will use a fragment of the Calculus of constructions, namely Gödel's System T (simply typed $\lambda$-calculus, natural numbers, and primitive recursion on them), so the argument applies to a ...


7

Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes. Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.


7

As Andrej has said, the problem is undecidable if you allow replacing one term by another, extensionally equal one. However, you might be interested in optimal sharing of expressions, in the following sense: given the reduction $$(\lambda x:T.C\ x\ x)\ u\rightarrow_\beta C\ u\ u $$ it is clear that the occurrences of the term $u$ can be shared in memory, and ...


6

Here is a slightly more explicit version of what Andreas said. The term $(\lambda x . x x) (\lambda x . x x)$ is not normalizing because it has exactly one $\beta$-redex, and when we reduce it we get back to the same term. But this term has the type $T$ for any type $T$ satisfying $T = T \to T$.


6

If you implement an evaluator for the terms of a language $A$ in a total system $B$, and you have furthermore proven that your evaluator is correct, that is for every $t$ well-typed in $A$, $$\mathrm{eval}(t) \simeq_A t $$ where $\simeq_A$ is the equality in $A$, then you have only shown that $\simeq_A$ is decidable. If furthermore $\simeq_A$ naturally ...


6

Let me insist on the viewpoint touched upon by cody's answer. As far a see it, the question of finding a smallest $\lambda$-term equivalent to another $\lambda$-term is not really interesting, even if it there were an algorithm computing it. In fact, most programs you write in the $\lambda$-calculus (or whatever calculus of the $\lambda$-cube) are already ...


5

Typically, fast growing hierarchies are characterized by ordinal notations, which are really just ways to express fast-growing functions (but it's sometimes convenient to see them as ordinals in the mathematical sense). There is a somewhat generic way of assigning an ordinal (notation) to a consistent theory, though it is very non-constructive. For various ...


5

I'd like to offer some pointers. Is there any research that goes along these lines and perhaps formalizes this intuition? Parametricity by analysis of the shape of (simply-typed) normal forms preceded by a normalisation argument was proposed by Girard, Scedrov, and Scott [1]. This connects parametricity, cut-elimination in logic, and a proof technique ...


4

I thought this might be tough, given the fact that the proof usually goes in the other direction (Parametricity $\Rightarrow$ Normalization), and the post by Gabriel is somewhat involved, but in system F one can do a relatively straightforward induction. I'm going to assume you're somewhat familiar with the usual statement of parametricty, e.g. from the "...


2

As usual, the bible knows all, and Lemma 3.3.8 (p 66) gives the detailed proof of commutativity of $\beta$ and $\eta$ reductions. Trying to reproduce it here would be tedious and wouldn't do it justice, so I'll include a picture: You had the main idea right, it just takes a bit of practice to generalize from the specific examples.


2

You can find the proof in Penttonen's original research article: Martti Penttonen, One-Sided and Two-Sided Context in Formal Grammars. Information and Control 25, pp. 371-392 (1974). https://doi.org/10.1016/S0019-9958(74)91049-3


Only top voted, non community-wiki answers of a minimum length are eligible