OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more

Tag Info

Hot answers tagged lambda-calculus

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

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

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 ...
• 11.5k
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 ...
• 29k
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: ...
• 11.5k

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 ...
• 261

• 13.9k

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 ...
• 1,187

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$ (...
• 29k

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