# Questions tagged [lambda-calculus]

Church's formal system used in computatability, programming languages and proof theory to represent effective functions, programs and their computation, and proofs.

225 questions
Filter by
Sorted by
Tagged with
716 views

### Equivalent formulation of complexity theory in Lambda Calculus?

In complexity theory the definition of time and space complexity both reference a universal Turing machine: resp. the number of steps before halting, and the number of cells on the tape touched. ...
1k views

### Why is lambda calculus a “calculus”?

The only definition of "calculus" I'm aware of is the study of limits, derivatives, integrals, etc. in analysis. In what sense is lambda calculus (or things like mu calculus) a "calculus"? How does it ...
280 views

### Calculus of Constructions: compress expression to its smallest form

I'm aware that the Calculus of Constructions is strongly normalizing, meaning every expression has a normal for that cannot be beta,eta-reduced further. So in fact this is the most efficient ...
471 views

### Does the System F with pairs have the strong normalisation and subject reduction properties?

It is easy to look in a lot of textbooks the proofs of subject reduction and strong normalisation for System F, also, sometimes there are definitions of System F with pairs, where (t,r) is a term, not ...
369 views

### Hereditary substitution with a universe hierarchy

I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types. I'm wondering, are there any examples of hereditary substitution in ...
1k views

### What is the “question” that programming language theory is trying to answer?

I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which ...
546 views

### What's the difference between reduction strategies and evaluation strategies?

From the evaluation strategy article on Wikipedia: The notion of reduction strategy in lambda calculus is similar but distinct. From the reduction strategy article on Wikipedia: It is similar ...
453 views

850 views

### Translation from basic While-language to $\lambda$-calculus

Is there a simple way to translate programs written in a basic "While" language (such as Winskels Imp)? I know about Church numerals and booleans, and I can see how if and while statements can be ...
385 views

### Are the $\lambda_I$-Calculus and the $\lambda_K$-Calculus equivalent?

I see here and there mention of the $\lambda_I$-Calculus (in which every variable must be used at least once) and the $\lambda_K$-Calculus (in which a variable can also be unused). Are they ...
975 views

### What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?

I've been reading Lectures on the Curry-Howard Isomorphism and it talks about intuitionistic/constructive logic (IL) , combinatory logic (CL) and lambda calculus ($\lambda$c) before moving on to the ...
In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...