45 votes

P and NP classes explanation through lambda-calculus

Turing-machines and $\lambda$-calculus are equivalent only w.r.t. the functions $\mathbb{N} \rightarrow \mathbb{N}$ they can define. From the point of view of computational complexity they seem to ...
user avatar
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 ...
user avatar
26 votes
Accepted

What was the original intent for the creation of Lambda calculus?

He wanted to create a formal system for the foundations of logic and mathematics that was simpler than Russell's type theory and Zermelo's set theory. The basic idea was to add a constant $\Xi$ to ...
user avatar
22 votes

Using lambda calculus to derive time complexity?

A recent developpement on this topic: U. dal Lago and B. Accatoli proved that the length of the leftmost-outermost reduction (LOr) of a $\lambda$-term is an invariant (time) cost model for $\lambda$-...
user avatar
  • 676
22 votes
Accepted

How exactly does lambda calculus capture the intuitive notion of computability?

You're in good company. Kurt Gödel criticized $\lambda$-calculus (as well as his own theory of general recursive functions) as not being a satisfactory notion of computability on the grounds that it ...
user avatar
  • 26.6k
22 votes
Accepted

Why it's impossible to declare an induction principle for Church numerals

The question you are asking is interesting and known. You are using the so-called impredicative encoding of the natural numbers. Let me explain a bit of the background. Given a type constructor $T : \...
user avatar
  • 26.6k
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. ...
user avatar
  • 13.2k
21 votes
Accepted

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

I will give a partial answer, I hope others will fill in the blanks. In typed $\lambda$-calculi, one may give a type to usual representations of data ($\mathsf{Nat}$ for Church (unary) integers, $\...
user avatar
21 votes

Is there a typed lambda calculus which is consistent and Turing complete?

Alright I'll give a crack at it: In general for a given type system $T$, the following is true: If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a ...
user avatar
  • 13.2k
20 votes
Accepted

Why do constructivists not seem to care too much about call/cc

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive ...
user avatar
  • 26.6k
19 votes
Accepted

Historic Relationship between Typed Lambda Calculus and Lisp?

First, your friend is wrong about the history of the $\lambda$-calculus. Church created the untyped calculus first, which he intended as a foundation for mathematics. Fairly quickly, it was discovered ...
user avatar
19 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 ...
user avatar
  • 13.2k
16 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 ...
user avatar
  • 26.6k
16 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: ...
user avatar
16 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 ...
user avatar
15 votes
Accepted

Scott's stochastic lambda calculi

One apparent strength of his approach is that it allows higher-order functions (i.e. lambda terms) to be observable outcomes, which measure theory generally makes quite tricky. (The basic problem is ...
user avatar
15 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 ...
user avatar
  • 251
14 votes
Accepted

Is this behavior in a programming language inconsistent?

Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it. Alpha-renaming the ...
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 ...
user avatar
14 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 ($\...
user avatar
13 votes

P and NP classes explanation through lambda-calculus

I paste part of an answer I wrote for another question: Implicit Computational Complexity aims at characterizing complexity classes by means of dedicated languages. The first results such as ...
user avatar
  • 4,400
13 votes

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

An answer to a question Damiano raised in his excellent answer: I am much more ignorant regarding the calculi obtained by just enabling dependent types (essentially Martin-Löf type theory without ...
user avatar
13 votes
Accepted

Contradiction between Gödel's Second Incompleteness Theorem and the Church-Rosser's property of CIC?

First, you are confusing consistency of CIC as an equational theory with consistency of CIC as a logical theory. The first means that not all terms of CIC (of the same type) are $\beta\eta$-equivalent....
user avatar
12 votes
Accepted

What is a term of the type $\bot\rightarrow A$?

There are several ways of writing such a term, depending on how we write the proof terms for the elimination rule for $\bot$, which is $$\frac{\quad\bot\quad}{A}$$ The corresponding rule in $\lambda$-...
user avatar
  • 26.6k
12 votes
Accepted

Can affine lambda calculus solve every problem in P?

Edit: my guess in the first paragraph below is wrong! Ugo Dal Lago pointed out to me a later paper by Martin Hofmann (appeared in POPL 2002), of which I was unaware, showing (as a corollary of more ...
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 ...
user avatar
11 votes
Accepted

Can factorial be encoded in the Kappa-calculus with fixed point operator?

The bare $\kappa$-calculus does not permit defining factorial, even when extended with a fixed point operator. However, this answer deserves some unpacking. The fixed point operator you give is not ...
user avatar
11 votes

Why do constructivists not seem to care too much about call/cc

As you note, there is a possible constructive interpretation of classical logic in this sense. The fact that classical logic is equiconsistent with intuitionistic logic (say, Heyting Arithmetic) has ...
user avatar
  • 13.2k
11 votes

Is there a typed lambda calculus which is consistent and Turing complete?

Here is an answer to a variant of @cody's precisification of my question. There is a consistent LPTS which is Turing complete in roughly @cody's sense, if we allow the introduction of additional ...
user avatar
11 votes

An example where smallest normal lambda term is not fastest

Blum’s speedup theorem is usually stated in the language of partially recursive functions, but up to trivial differences in notation, it works just the same in the language of $\lambda$-calculus. It ...
user avatar

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