# Tag Info

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 ... 8 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 ... 7 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 ...

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$.

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 ...

5

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 "...

4

May I have a reference to why η expansion is invalid for CoC? It's not invalid. It's up to choice whether $\eta$-conversion for functions (or other types) is included. The original CoC paper seems to omit it, but as you see ATAPL includes it. I'm not certain, but $\eta$ may have been omitted from the original source because it was difficult to handle in the ...

3

S(C(KM)M)I ~ MM suffices The reduction is as follows: S(C(KM)M)Ix C(KM)Mx(Ix) C(KM)Mxx KMxMx MMx

3

They are different things. SClos is a case-split function, which is a function that pattern match on its parameter. Think of it as a lambda (if you know Haskell, you can think of it as a LambdaCase \case, which is a sugared lambda). This is definitely a canonical value in Mini-TT. The neutral value, OTOH, is an application on a case-split function, where 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

2

IMHO universe hierarchy is particularly complicated to implement while the benefit is very small. It complicates programming in the language and the implementation of the language. The only benefit is to ensure the logical consistency. I guess that's why everybody is not writing about it. Here are some answers to your questions. I don't know much type theory ...

1

I have a shorter answer: normalization is usually used in conversion check of terms (aka definitional equality), and CoC has untyped conversion check. In conversion check, we normalize terms and compare 'em syntactically (think of it as comparing the ASTs). This probably means the normalization process doesn't have access to the types of terms, so it may not ...

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