# 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.

40 questions
Filter by
Sorted by
Tagged with
9k views

### Realizability theory: difference in power between Lambda calculus and Turing Machines

I have three related subquestions, which are highlighted by bullet points below (no, they could not be split, if you are wondering). Andrej Bauer wrote, here, that some functions are realizable ...
28k views

### Relationship between Turing Machine and Lambda calculus?

Is there a relationship between the Turing Machine and the Lambda calculus - or did they just happen to arise about the same time?
5k views

### Using lambda calculus to derive time complexity?

Are there any benefits to calculating the time complexity of an algorithm using lambda calculus? Or is there another system designed for this purpose? Any references would be appreciated.
3k views

### Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
1k views

### Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
454 views

### Extensions of beta-theory of lambda calculus

The beta-eta-theory of the lambda-calculus is Post-complete. Can additional rules be added to extend the beta-theory of the lambda-calculus to get confluent theories other than the beta-eta theory? ...
318 views

### Characterising invisible equivalences by confluent rewrite rules

In response to another question, Extensions of beta theory of lambda calculus, Evgenij offered the answer: beta + the rule {s = t | s and t are closed unsolvable terms} where a term M is solvable if ...
484 views

### Incomplete basis of combinators

This is inspired by this question. Let $\mathcal{C}$ be the collection of all combinators which only have two bound variables. Is $\mathcal{C}$ combinatorially complete? I believe the answer is ...
340 views

### What is the benefit of Krivine's notation?

I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus. For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ ...
869 views

### What does it mean that there are differing views on how computations are represented on the Turing Machine?

For a given algorithm (eg reverse the items in this list) and a given type of Turing machine (eg the 3-state 2-symbol busy beaver reduced to 5-tuples) - is there a single simplest way that this ...
30k views

### What is the contribution of lambda calculus to the field of theory of computation?

I'm just reading up on lambda calculus to "get to know it". I see it as an alternate form of computation as opposed to the Turing Machine. It's an interesting way of doing things with functions/...
7k views

### P and NP classes explanation through lambda-calculus

In the introduction and explanation P and NP complexity classes often given through Turing machine. One of the model of computation is the lambda-calculus. I understand, that all of models of ...
1k views

### Is there a non Turing-complete model of computation whose halting problem is undecidable?

I cannot think of any such model, maybe some form of typed lambda calculus? some elementary cellular automaton? This would almost disprove Wolfram's "Principle of Computational Equivalence": ...
2k views