9 votes
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 ...
user avatar
9 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 ...
user avatar
8 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 ...
user avatar
  • 13.2k
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 ...
user avatar
  • 26.6k
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 :...
user avatar
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 ...
user avatar
  • 13.2k
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{...
user avatar
  • 13.2k
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 ...
user avatar
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 ...
user avatar
6 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 ...
user avatar
  • 26.6k
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 ...
user avatar
  • 13.2k
5 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 ...
user avatar
  • 112
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 ...
user avatar
  • 13.2k
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
user avatar
  • 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, ...
user avatar
  • 923
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 ...
user avatar
  • 13.2k
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/...
user avatar
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 ...
user avatar
  • 923
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 ...
user avatar
  • 923

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