35 votes
Accepted

How do you get the Calculus of Constructions from the other points in the Lambda Cube?

First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is based on) is very different from the Calculus of Constructions. It is best thought of as ...
Neel Krishnaswami's user avatar
22 votes

How do you get the Calculus of Constructions from the other points in the Lambda Cube?

I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot. But first, one should probably try to dis-entangle various issues. ...
cody's user avatar
  • 13.9k
12 votes
Accepted

Is there an efficient beta-equivalence algorithm?

The answer is no. An old theorem of Statman states that $\beta$-equivalence in the simply-typed $\lambda$-calculus is not elementary recursive, that is, no algorithm whose running time is bounded by $...
Damiano Mazza's user avatar
9 votes
Accepted

Proof techniques for showing that dependent type checking is decidable

There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why ...
cody's user avatar
  • 13.9k
9 votes
Accepted

Recursive types and the empty type

First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, ...
Neel Krishnaswami's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.9k
8 votes
Accepted

Complexity of type inference in the simply typed lambda calculus

Type inference for simply typed lambda calculus is complete for polynomial time, as elegantly explained in section 1 of Harry Mairson's Linear lambda calculus and PTIME-completeness. To be a bit more ...
Noam Zeilberger's user avatar
8 votes
Accepted

Are there strongly normalizing lambda terms that cannot be given a System F type?

As you found out yourself, the answer to your question is yes. You found a rather convoluted example, a much simpler example is the following: $$(\lambda zy.y(zI)(zK))(\lambda x.xx)$$ where $I$ and $...
Damiano Mazza's user avatar
7 votes
Accepted

Understanding the Proof of Strong Normalization of the Calculus of Constructions

Unfortunately, I'm not sure there are more beginner friendly resources than Geuvers' account. You might try this note from Chris Casinghino which gives an account of several proofs in excruciating ...
cody's user avatar
  • 13.9k
7 votes
Accepted

Typing of substitution in a bidirectional type system

The key observation is that whether the substitution theorem holds, depends on the definition of substitution. For the usual definition of substitution of terms for variables, the substitution ...
Neel Krishnaswami's user avatar
7 votes

Typing of substitution in a bidirectional type system

One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't ...
gallais's user avatar
  • 635
7 votes
Accepted

Structural equality of Pi Types with heterogeneous equality?

I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type: ...
András Kovács's user avatar
7 votes

Eta expansion in the pattern lambda calculus

This is not a complete answer; it is a comment that got too large. If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators ...
Neel Krishnaswami's user avatar
7 votes
Accepted

Is simply typed lambda calculus equivalent to primitive recursive functions

The simply-typed λ-calculus with β-equality at type (o → o) → o → o (which can be seen as type of the natural numbers, whenever o is any base type) can define exactly the extended polynomials (= ...
Martin Berger'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 ...
cody's user avatar
  • 13.9k
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 ...
Damiano Mazza's user avatar
6 votes

What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?

Yes, in general $\mathrm{Id}_{A}(x, y)$ will not have a canonical form. Consider the case when $x$ and $y$ are distinct free variables -- obviously you can postulate that $x$ and $y$ are equal, but ...
Neel Krishnaswami's user avatar
6 votes

Type checking, Hypothetical judgments, meaning explanations and computational type theory

Part of the problem is we cannot say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ ...
Jonathan Sterling's user avatar
6 votes
Accepted

Enumerating all simply typed lambda terms of a given type

This question has been considered several times in the academic community, from the practical: Yakushev & Jeuring, Enumerating Well-Typed Terms Generically Fetsher & al, Making Random ...
cody's user avatar
  • 13.9k
6 votes
Accepted

Termination checking for Scott-encodings in System F with positive-recursive types

I'll first point you to Types for the Scott Numerals by Plotkin, Cardelli and Abadi, where they show how to encode Scott numerals in plain old system F. This at least shows that you can write the "...
cody's user avatar
  • 13.9k
6 votes

Is there an efficient beta-equivalence algorithm?

I'd like to point out that if: the terms $M$ and $N$ are strongly normalizing (as the question allows), and one considers the complexity as depending also on the number $k_M$ and $k_N$ of beta-steps ...
Beniamino Accattoli's user avatar
6 votes

Model of MLTT with $\eta$ rule where function extensionality fails

The simplest one that I know about is the $\text{Set}$-based polynomial model ("container" model). Here, every context is interpreted as a family of sets, i.e. a $Q : \text{Set}$ together ...
András Kovács's user avatar
6 votes

Complexity of convertibility in simply typed λ-calculus with sums

(Gabriel Scherer reporting.) I'm not a complexity person, so my answer will be partial. Here is what I can tell in short amount of thinking: You mention that the arrow(,product) case is TOWER-...
gasche's user avatar
  • 2,040
6 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/...
Damiano Mazza's user avatar
5 votes

Moggi's computational metalanguage

It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For ...
Andrej Bauer's user avatar
  • 28.9k
5 votes

Can typed lambda calculi express *all* algorithms below a given complexity?

Two complements to Damiano's answer: in the simply typed λ-calculus, the expressible functions depend very much on the input and output representations, and for instance there is a way to make all ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
5 votes

Program inversion algorithms for higher-order programs

There hasn't been a huge amount of work in this space, but what work there is, is pretty interesting. Torben Mogensen has worked on this problem. Here are two papers of his. The first paper gives ...
Neel Krishnaswami's user avatar
5 votes
Accepted

Decidability of rank-k polymorphism vs. System F

The conclusion of [Kfoury & Tiuryn 1992] says (emphasis mine): We prove that [...] for every $k\ge 3$ there is a typing of constants that assigns types in $S(1)$ such that the type ...
Radu GRIGore's user avatar
  • 4,796
5 votes
Accepted

What arithmetical theorems can plain $\lambda \Pi$ reason about?

As Andrej notes, $\lambda\Pi$ is a conservative extension of first-order logic which means: Adding the axioms of PA to $\lambda\Pi$ gives exactly the same arithmetic theorems as PA. However, ...
cody's user avatar
  • 13.9k
5 votes
Accepted

Generalizations, or extensions of W-types in MLTT

The representation issue of W-types was resolved by Jasper Hugunin. So from type formers $0$, $1$, $2$, $W$, $\Pi$, $\Sigma$, identity and a universe hierarchy we do get all indexed inductive families ...
András Kovács's user avatar

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