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
94
votes
7
answers
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/...
- 5,255
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
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
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
44
votes
3
answers
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 ...
- 541
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
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
25
votes
2
answers
4k
views
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems ...
- 353
25
votes
1
answer
2k
views
What's the expressive power of Simply Typed Lambda calculus?
The standard approach to simply typed lambda calculus considers computations over Church numerals.
If input and outputs are Church numerals always typed as $Int$, where $Int = (\tau \rightarrow \tau) ...
- 411
23
votes
4
answers
1k
views
Can typed lambda calculi express *all* algorithms below a given complexity?
I know that the complexity of most varieties of typed lambda calculi without the Y combinator primitive is bounded, i.e. only functions of bounded complexity can be expressed, with the bound becoming ...
- 8,921
23
votes
4
answers
4k
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 ...
- 604
23
votes
2
answers
2k
views
What was the original intent for the creation of Lambda calculus?
I've read that initially Church proposed the $\lambda$-calculus as part of his Postulates of Logic paper (which is a dense read). But Kleene proved his "system" inconsistent after which, Church ...
- 5,255
22
votes
1
answer
2k
views
What is the difference between arrows and exponential objects in a cartesian closed category?
In a Cartesian Closed Category (CCC), there exist the so-called exponential objects, written $B^A$. When a CCC is considered as a model of the simply-typed $\lambda$-calculus, an exponential object ...
- 2,775
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
21
votes
1
answer
2k
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:
...
- 1,762
21
votes
1
answer
622
views
A Lambda calculus for invertible (r-Turing computable) functions
I'm interested in the concept of "r-Turing completeness", as defined by Axelsen and Glück (2011). A system is r-Turing complete if it can compute the same set of functions as a reversible Turing ...
- 699
20
votes
2
answers
2k
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 ...
- 461
20
votes
2
answers
2k
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 ...
- 652
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
19
votes
1
answer
908
views
Scott's stochastic lambda calculi
Recently, Dana Scott proposed stochastic lambda calculus, an attempt to introduce probabilistic elements into (untyped) lambda calculus based on a semantics called graph model. You can find his ...
- 895
18
votes
3
answers
1k
views
funsplit and polarity of Pi-types
In a recent thread on the Agda mailing list, the
question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark.
My understanding is that $\eta$ laws come with negative
...
- 478
18
votes
2
answers
782
views
Is it possible to decide $\beta$-equivalence within System F (or another normalizing typed λ-calculus)?
I know that's impossible to decide $\beta$-equivalence for untyped lambda calculus. Quoting Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984).:
If A ...
- 2,571
18
votes
1
answer
3k
views
Historic Relationship between Typed Lambda Calculus and Lisp?
I was having a discussion with a friend recently (who is an advocate of strongly typed languages). He made the comment:
The inventors of Lambda Calculus always intended it to be typed.
Now we can ...
- 2,581
17
votes
2
answers
2k
views
How is Lambda Calculus a specific type of Term Writing system?
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 Calculus.
When John ...
- 2,581
17
votes
1
answer
1k
views
How can non-terminating $\lambda$-terms be turned into fixed-point combinators?
I've been thinking about these questions:
Is there a typed lambda calculus which is consistent and Turing complete?
https://cs.stackexchange.com/questions/65003/if-%CE%BB-x-x-x-has-a-type-then-is-...
- 13.7k
16
votes
6
answers
2k
views
What is the point of calling $\lambda$-calculus an algebra?
What is the difference of calling $\lambda$-calculus an algebra instead of a calculus? I raise this question because I read somewhere the line "$\lambda$-calculus is not a calculus but an algebra" (...
- 2,775
16
votes
3
answers
1k
views
Why do constructivists not seem to care too much about call/cc
So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't ...
- 1,141
16
votes
3
answers
1k
views
Can we prove weak normalization for System F by induction on a transfinite ordinal
Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
user6892
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
16
votes
1
answer
1k
views
Can we derive Cubical Type Theory from Self-Types?
Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded&...
- 3,117
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
16
votes
1
answer
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.
...
- 261
15
votes
2
answers
483
views
(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?
From a purely abstract math/computational reasoning point of view, (how) could one even discover or reason about problems like 3-SAT, Subset Sum, Traveling Salesman etc.,? Would we be even able to ...
- 5,255
15
votes
2
answers
2k
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 ...
- 269
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
15
votes
2
answers
1k
views
Fixed points in computability and logic
This question has also been posted on Math.SE,
https://math.stackexchange.com/questions/1002540/fixed-points-in-computability-nd-logic
I hope it is ok to also post it here. If not, or if it is too ...
- 151
14
votes
2
answers
477
views
Church-Rosser property for dependently typed lambda calculus?
It is well-known that the Church-Rosser property holds for $\beta \eta$-reduction in simply-typed lambda calculus. This implies that the calculus is consistent, in the sense that not all equations ...
- 777
14
votes
1
answer
509
views
Lambda-Calculus terms that reduce to themselves
In my continuing quest to try to learn lambda calculus, Hindley & Seldin's "Lambda-Calculus and Combinators an Introduction" mentions the following paper (by Bruce Lercher) which proves that the ...
- 191
14
votes
1
answer
1k
views
η-conversion vs extensionality in extensions of lambda-calculus
I'm often confused by the relation between η-conversion and extensionality.
Edit: According to comments, it seems I'm also confused about the relation between extensional equivalence and ...
- 2,049
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
14
votes
0
answers
419
views
Are there simple core languages which are consistent and expressive?
The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
- 3,117
14
votes
0
answers
257
views
historical question: earliest description of beta-normal terms together with "neutral" terms in lambda calculus?
A bit of "folklore" in lambda calculus is the idea of characterizing the class of $\beta$-normal terms inductively as a syntactic category ($R$) defined in mutual induction with an auxiliary syntactic ...
- 4,431
13
votes
6
answers
3k
views
Functions that typed lambda calculus cannot compute
I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi.
As I am a beginner, some reiteration of background information ...
- 201
13
votes
5
answers
600
views
Representing bound variables with a function from uses to binders
The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de ...
- 675
13
votes
2
answers
1k
views
How exactly does lambda calculus capture the intuitive notion of computability?
I've been trying to wrap my head around the what, why and how of $\lambda$-calculus but I'm unable to come to grips with "why does it work"?
"Intuitively" I get the computability model of Turing ...
- 5,255
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
13
votes
3
answers
843
views
What are the negative consequences of extending CIC with axioms?
Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term ...
- 777
13
votes
1
answer
2k
views
Can Scheme's call/cc implement all known control flow structures?
The page "Advanced Scheme: Some Naughty Bits" states:
Continuations are a powerful control-flow construct from which
nearly any other control-flow structure [...] may be derived.
I thought that ...
- 133
12
votes
3
answers
2k
views
How to make the Lambda Calculus strong normalizing without a type system?
Is there any system similar to the lambda calculus that is strong normalizing, without the need to add a type system on top of it?
- 3,117
12
votes
1
answer
4k
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 ...
- 5,255