Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more
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
22 votes
Accepted

How is Lambda Calculus a specific type of Term Writing system?

The answer is it depends what you mean by Term Rewrite System. When it was introduced, the concept of Term Rewrite Systems, or TRSes, described what is now called first order TRSes, which is simply a ...
cody's user avatar
  • 13.9k
19 votes

What is the "question" that programming language theory is trying to answer?

The overall purpose of PLT is to make industrial software engineering (in a general sense) cheaper (also in a general sense), through optimising the most important tool (programming languages) and ...
Martin Berger's user avatar
18 votes
Accepted

(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

You may wish to look at cost semantics for functional languages. These are various computational complexity measures for functional languages that do not pass through any kind of Turing machine, RAM ...
Andrej Bauer's user avatar
17 votes
Accepted

Equivalent formulation of complexity theory in Lambda Calculus?

As you point out, the λ-calculus has a seemingly simple notion of time-complexity: just count the number of β-reduction steps. Unfortunately, things are not simple. We should ask: ...
Martin Berger's user avatar
16 votes

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

To me, your question seems analogous to saying "I've heard that non-Euclidean geometry requires me to give up Euclid's fifth axiom, which is very useful in many mathematical contexts." You don't have ...
Alexis's user avatar
  • 261
15 votes

(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

At the request of Andrej and PhD, I am turning my comment into an answer, with apologies for self-advertising. I recently wrote a paper in which I look at how to prove the Cook-Levin theorem ($\...
Damiano Mazza's user avatar
14 votes
Accepted

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

You seem to be confusing several things here. First of all, like Alexis said in her answer, I don't see why you would need to accept/reject the principles of a given logical theory in order to study ...
Damiano Mazza's user avatar
13 votes
Accepted

Does the Law of Excluded Middle imply the Axiom K in Martin-Löf's Intensional Type Theory?

Yes, LEM implies K. See HoTT book Theorem 7.2.5, known as Hedberg's theorem, which shows that any type with decidable equality satisfies axiom $K$. If we assume excluded middle, all types have ...
Andrej Bauer's user avatar
13 votes
Accepted

Is a CEK machine an implementation of a CESK machine?

The store in a CESK machine is the “heap”, where mutable pointer-based data structures live. If your language is purely functional, then its operational semantics don’t need a store. Take it out, ...
Neel Krishnaswami's user avatar
12 votes

Incomplete basis of combinators

[Expanding the comment into an answer.] First, just a clarification about counting bound variables in a combinator (= closed term) $t$. I interpret the question as asking about $$ \text{the total ...
Noam Zeilberger's user avatar
12 votes

Representing bound variables with a function from uses to binders

Andrej's and Łukasz's answers make good points, but I wanted to add additional comments. To echo what Damiano said, this way of representing binding using pointers is the one suggested by proof-nets, ...
Noam Zeilberger's user avatar
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
11 votes

Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?

Type theory is a mathematical theory in which we can do very many different things (set theory is like that as well). We can use type theory for computability, or homotopy theory, or use it to express ...
Andrej Bauer's user avatar
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 ...
Andreas Rossberg's user avatar
11 votes

Applications of Barendregt–Geuvers–Klop conjecture

I'm not (exactly) an expert, but my understanding is that there are very few practical applications of this conjecture, except possibly simplifying the decision procedure for type-checking in ...
cody's user avatar
  • 13.9k
11 votes

$\eta$-reduction not locally confluent on well-typed terms

Yes, $\eta$ reduction for unit is terribly behaved. Suppose you are in a context $\Gamma \triangleq x:1, y:1$. Then, the unit term $\Gamma \vdash \left\langle\right\rangle : 1$ has the following eta-...
Neel Krishnaswami's user avatar
11 votes

What are pertinent references to cite on Scott domains?

I asked Dana Scott who kindly responded. I am relaying his answer: I think the paper “A type-theoretical alternative to ISWIM, CUCH, OWHY” answers the questions and gives the context of the discovery....
Andrej Bauer's user avatar
10 votes

What's the expressive power of Simply Typed Lambda calculus?

As explained by Damiano Mazza here on MathOverflow (see also this TCS.SE question), for a very natural choice of encodings of input strings and output booleans, one gets exactly the regular languages! ...
Lê Thành Dũng 'Tito' Nguyễn's user avatar
10 votes
Accepted

Why is the multi-step reduction of semantics reflexive?

The practical reason is that it is very convenient to include also the case "zero steps" in the definition of "many steps" (millennia of mathematical experience have taught us that it is usually a ...
Damiano Mazza's user avatar
10 votes
Accepted

Can a totality checker be used to guarantee a proof on the calculus of constructions + inductive types is correct?

I'm going to assume that by $\mathrm{Fix}$ you mean a new type constructor $$\frac{\Gamma\vdash F:*\rightarrow *}{\Gamma\vdash \mathrm{Fix}\ F:*} $$ Along with the conversion rule $\mathrm{Fix}\ F\...
cody's user avatar
  • 13.9k
10 votes

Representing bound variables with a function from uses to binders

I'm not sure how your variable-to-binder-function would be represented and for what purpose you'd like to use it. If you are using back-pointers then as Andrej noted the computational complexity of ...
Łukasz Lew's user avatar
  • 1,187
10 votes

Preservation under Substitution with Telescopes

The most general form of substitution theorems speaks about arbitrary contexts: Define what it means to have a substitution $\sigma : \Gamma \to \Delta$ from a context $\Gamma$ to a context $\Delta$ (...
Andrej Bauer's user avatar
10 votes

Can we derive Cubical Type Theory from Self-Types?

This is not an answer but a very long comment. I find the idea quite interesting. To keep things focused, I think it would be very good to have a clear idea of what it means for the encoding of ...
Andrej Bauer's user avatar
9 votes

Understanding between lambda-calculus and other abstract machines (like Turing machine and Markov algorithm)

There are essentially two ways to describe a computational model: by describing a low level arhitectural model and its command language, that is the case of Turing Machines, Random Access Machines, ...
Andrea Asperti's user avatar
9 votes
Accepted

How can non-terminating $\lambda$-terms be turned into fixed-point combinators?

There are several aspects to this very nice question, so I will structure this answer accordingly. $\newcommand{\setof}[1]{\{#1\}}$ $\newcommand{\thra}{\twoheadrightarrow}$ $\newcommand{\codeof}[1]{\...
Andrew Polonsky's user avatar
9 votes
Accepted

Can you assign a type to any term of the λEA-calculus?

For question 1, the answer is no, and is no for almost any type discipline (except certain intersection types): the fact that a term is (strongly or weakly) normalizable does not imply in general that ...
Damiano Mazza's user avatar
9 votes

Is it possible to create a "quote" function that, given a native λ-term, returns its λ-encoded representation?

No, this is not possible, assuming you want to go from an arbitrary lambda term to some first-order AST. The lambda calculus is extensional, which means that the lambda calculus cannot distinguish ...
Neel Krishnaswami's user avatar
9 votes

Equivalent formulation of complexity theory in Lambda Calculus?

Counting $\beta$-reductions is one kind of complexity measure for $\lambda$-calculus, but a more flexible and reasonable one is cost semantics, where the operational semantics is augmented by various ...
Andrej Bauer's user avatar

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