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
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
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
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
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
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
12
votes
1
answer
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 ...
- 259
9
votes
2
answers
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$ ...
- 2,775
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
12
votes
1
answer
454
views
An example where smallest normal lambda term is not fastest
Let the $size$ of $\lambda$-terms be defined as follows:
$size(x) = 1$,
$size(λx.t) = size(t) + 1$,
$size(t s) = size(t) + size(s) + 1$.
Let the complexity of a $\lambda$-term $t$ be defined as
the ...
- 3,117
12
votes
1
answer
880
views
Can affine lambda calculus solve every problem in P?
In Advanced Topics in Types and Programming Languages it is mentioned, in the chapter on sub-structural type systems, that a "carefully crafted" affine lambda calculus with a recursion combinator for ...
- 1,141
11
votes
2
answers
438
views
Hereditary substitution with a universe hierarchy
I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types.
I'm wondering, are there any examples of hereditary substitution in ...
- 2,830
10
votes
1
answer
409
views
8
votes
0
answers
179
views
deciding $\beta$-equality of planar lambda terms
Mairson showed that the problem of computing the $\beta$-normal form of a linear lambda term (or equivalently, computing its principal type) is complete for polynomial time.
Harry Mairson. Linear ...
- 4,431
8
votes
8
answers
8k
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?
- 121
7
votes
1
answer
747
views
Fixed points in dependent type theories
Most dependent type theories aim for some notion of correctness in two respects:
The type system must be decidable.
The type system must be consistent. e.g. $\forall \tau. \tau$ should not be ...
- 1,141
7
votes
1
answer
233
views
Is it possible to unambiguously read back λ terms from interaction nets without node types?
A class of lambda terms can be evaluated using Lamping's abstract algorithm - that is, converting them to interaction nets and applying a set of rules. In order to get the result, you have to read ...
- 3,117
4
votes
0
answers
169
views
Hereditary Substitution with Inductives and Eliminators?
I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators?
In particular, normalizing the application of an eliminator to an ...
- 2,830
4
votes
0
answers
519
views
Is it possible to derive induction by extending CoC with recursion?
Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms:
...
- 3,117
4
votes
1
answer
357
views
Locally-nameless normalization
This paper on locally-nameless (Charguéraud, Arthur: The locally nameless representation, Journal of Automated Reasoning (2012): 1-46) describes how to perform beta-reduction by "opening", but it's ...
- 701
4
votes
1
answer
295
views
What is a term of the type $\bot\rightarrow A$?
The sentence $\bot\rightarrow A$ is provable in intuitionistic logic for any type $A$. The proof is trivial:
\begin{align}
\bot&\vdash\bot \\
\hline
\bot&\vdash A \\
\hline
&\vdash\bot\...
- 143
3
votes
0
answers
368
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, ...
- 3,117
1
vote
0
answers
47
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 ...
- 3,117