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

37 questions
Filter by
Sorted by
Tagged with
2answers
7k 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 ...
5answers
19k 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?
7answers
3k 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.
3answers
2k 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 ...
1answer
394 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? ...
1answer
918 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. ...
3answers
742 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 ...
1answer
270 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 ...
2answers
293 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$ ...
7answers
28k 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/...
2answers
1k views

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

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function? This ...
4answers
3k views

### What's the point of $\eta$-conversion in lambda calculus?

I think I'm not understanding it, but $\eta$-conversion looks to me as a $\beta$-conversion that does nothing, a special case of $\beta$-conversion where the result is just the term in the lambda ...
1answer
888 views

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

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way: ...
2answers
894 views

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

Now we can see that Church was associated with the Simply Typed Lambda Calculus. Indeed, it seems he explained the Simply Typed Lambda Calculus in order to reduce misunderstanding about the Lambda ...
4answers
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": ...
2answers
945 views

### Smallest possible universal combinator

I am looking for the smallest possible universal combinator, measured by the number of abstractions and applications required to specify such a combinator in the lambda calculus. Examples of universal ...
8answers
4k views

### What are the simplest turing-complete systems? [closed]

Lambda Calculus is very simple. Are there even simpler turing-complete systems? Which is the simplest of them all?
0answers
1k views

0answers
98 views

### Is it possible to check equality of equi-recursive types, or recursive λ-terms?

Can we determine if two λ-terms are equal? Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, ...
0answers
40 views

### Is it possible to use arbitrary fixpoint values on EAL without losing strong normalization?

From this question, the answerer states EAL-based languages can use arbitrary fixpoint types without losing strong normalization, because their normalization (and complexity) properties comes from ...