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.

Filter by
Sorted by
Tagged with
13 votes
2 answers

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{\...
Ohad Kammar's user avatar
  • 2,667
7 votes
2 answers

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 ...
aioobe's user avatar
  • 181
19 votes
3 answers

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 ...
jon_darkstar's user avatar
16 votes
1 answer

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 ...
kow's user avatar
  • 163
26 votes
4 answers

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": ...
didest's user avatar
  • 1,551
15 votes
2 answers

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 ...
Charles Stewart's user avatar
60 votes
3 answers

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 ...
Blaisorblade's user avatar
  • 2,049
7 votes
3 answers

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 ...
hawkeye's user avatar
  • 2,581
11 votes
2 answers

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 ...
Alejandro DC's user avatar
54 votes
5 answers

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?
hawkeye's user avatar
  • 2,581
21 votes
3 answers

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):
hawkeye's user avatar
  • 2,581
14 votes
1 answer

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 ...
Charles Stewart's user avatar
44 votes
7 answers

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.
Shane's user avatar
  • 2,233
30 votes
2 answers

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 ...
Shane's user avatar
  • 2,233
16 votes
1 answer

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? ...
Charles Stewart's user avatar

1 2 3 4 5