11
votes
Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?
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 ...
- 1,320
10
votes
Accepted
Strong normalization property of CoC inside CoC
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 ...
- 14k
8
votes
Accepted
The precise definition of Normalization By Evaluation?
The difference you see between higher-order and closure-based representations is a lot smaller than it first seems: the closure-based representation arises as the defunctionalisation of the higher-...
- 32.8k
8
votes
Accepted
Is there a formalization of normalization of impredicative system F?
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 :...
- 32.8k
8
votes
Accepted
Calculus of Constructions: compress expression to its smallest form
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 ...
- 29.4k
7
votes
Accepted
Lambda-calculus: Beta-equivalent terms have the same type
The answer depends on what you mean by "simply-typed $\lambda$-calculus". There are two possibilities:
Church-style: in this formulation, terms explicitly carry their type and reduction/...
- 5,598
7
votes
Accepted
What's the difference between proving weak normalization and implementing evaluator?
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{...
- 14k
7
votes
Proof that the calculus of constructions extended with recursive types isn't strongly normalizing?
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 ...
- 29.4k
7
votes
Calculus of Constructions: compress expression to its smallest form
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 ...
- 14k
7
votes
Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?
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 ...
- 317
6
votes
Accepted
What technique is used to implement type checking for CoC?
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 ...
- 1,639
6
votes
Calculus of Constructions: compress expression to its smallest form
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 ...
- 5,598
5
votes
Accepted
Is there a 'very fast growing' hierarchy that would capture System F?
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 ...
- 14k
5
votes
Accepted
Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?
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 ...
- 14k
5
votes
Accepted
Defining normalization with respect to judgmental equality instead of reduction
You could define a predicate $N(t)$ whose intuitive meaning is “term $t$ is in normal form”, and prove a theorem stating that for every closed term $t$ there is precisely one term $t'$ such that $N(t')...
- 29.4k
3
votes
Lambda-calculus: Beta-equivalent terms have the same type
Actually I have deleted an answer to what I claimed in the comments and would like to provide a counterexample in Curry-style STLC, this is 5.12 in
https://www.cse.chalmers.se/research/group/logic/...
- 920
3
votes
Accepted
Can a normal form term be extensionally equivalent to a term with no WHNF?
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
- 916
3
votes
Accepted
NBE for MiniTT: Why is labelled sum eliminator both a normal form and a neutral value?
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, ...
- 965
2
votes
Converting Kuroda normal form rules to the Penttonen normal form
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/...
- 6,665
2
votes
Infinite $\beta \eta$-reduction sequence implies infinite $\beta$-reduction sequence
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 ...
- 14k
2
votes
Accepted
References on implementing universe levels over MLTT?
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 ...
- 965
1
vote
What technique is used to implement type checking for CoC?
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 ...
- 965
Only top scored, non community-wiki answers of a minimum length are eligible