# Tag Info

### 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
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
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
Accepted

• 29.4k

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

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

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