# Tag Info

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 ...
• 13.5k

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

### What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?

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 ...
• 10.6k
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 ...
• 27.6k
Accepted

• 27.6k
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, ...
• 945

### 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/...
• 841

### 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 ...
• 13.5k

### 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/...
• 5,534
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 ...
• 945
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 ...
• 945

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