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.
265
questions
13
votes
2
answers
506
views
What are the equational laws for zero types?
Disclaimer: while I care about type theory, I don't consider myself an expert on type theory.
In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator:
$$\frac{\...
- 2,667
7
votes
2
answers
955
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 ...
- 181
19
votes
3
answers
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 ...
- 293
16
votes
1
answer
572
views
Are innermost reductions perpetual in untyped λ-calculus?
(I have already asked this at MathOverflow, but got no answers there.)
Background
In the untyped lambda calculus, a term may contain many redexes, and different choices about which one to reduce may ...
- 163
26
votes
4
answers
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":
...
- 1,551
15
votes
2
answers
512
views
Are there intermediate eta theories for the lambda calculus?
There are two main, studied theories of the lambda calculus, the beta theory and its Post-complete extension, the beta-eta theory.
Do these two theories have an in-between, a kind of intermediate eta ...
- 4,306
60
votes
3
answers
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 ...
- 2,049
7
votes
3
answers
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 ...
- 2,581
11
votes
2
answers
491
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 ...
- 701
54
votes
5
answers
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?
- 2,581
21
votes
3
answers
2k
views
Why can Lambda Calculus not represent some combinators?
This paper suggests that there are combinators (representing symbolic computations) that can not be represented by the Lambda calculus (if I understand things correctly):
- 2,581
14
votes
1
answer
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 ...
- 4,306
44
votes
7
answers
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.
- 2,233
30
votes
2
answers
4k
views
Are lambda calculus and combinatory logic the same?
I am currently reading "Lambda-Calculus and Combinators" by Hindley and Seldin. I'm not an expert, but have always taken an interest in lambda calculus because of involvement with functional ...
- 2,233
16
votes
1
answer
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?
...
- 4,306