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
1
vote
0
answers
182
views
Optimal reduction using token-passing nets
I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in the spirit of "Token-Passing Nets: Call-by-Need for Free" by François-Régis ...
10
votes
2
answers
713
views
What's the difference between reduction strategies and evaluation strategies?
From the evaluation strategy article on Wikipedia:
The notion of reduction strategy in lambda calculus is similar but distinct.
From the reduction strategy article on Wikipedia:
It is similar ...
- 281
10
votes
1
answer
409
views
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
8
votes
1
answer
468
views
What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?
In lambda calculus or in combinatory logic we formally define reduction/expansion rules for terms (and in their typed variants reductions must preserve the type). Then we can talk about properties of ...
- 2,571
-2
votes
1
answer
424
views
What is the simplest known solver for a np-complete problem?
Lets define the simpler of two terms as the one with shortest description length on the untyped λ-calculus. Trying to find the simplest solver for a np-complete problem, I've got this:
...
- 3,117
10
votes
1
answer
905
views
How do you encode Lamping's abstract algorithm using interaction combinators?
Interaction combinators have been proposed as a compile target for the λ-calculus before. That paper implements the full λ-calculus. It is also known that it is possible to optimize interaction-net ...
- 3,117
2
votes
1
answer
179
views
Would a proof that the traveling salesman algorithm can't be encoded on LAL also prove P!=NP?
An answer to the traveling salesman (and similar) problems can be easily verified on light lambda-calculi. Also, if I understand correctly, the light lambda-calculi can compute every polinomial-time ...
- 3,117
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
1
answer
72
views
Is infinitary Böhm-reduction wrt. root-active terms for $\lambda$-calculus transitive?
I expect the answer to be "obviously yes", but to my inexperienced eye, that's not directly obvious, because the definition of infinite Böhm-reduction does not include a transitivity rule (it wouldn't ...
- 2,049
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
3
votes
1
answer
161
views
Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?
Let f and g be lambda terms in the normal form, such that f is intensionally different from <...
- 3,117
8
votes
2
answers
1k
views
Weakly normalizing + confluent = strongly normalizing?
I was reading this abstract and saw that they prove weak normalization and confluence. My limited understanding suggests that those two properties should provide strong normalization, which then ...
- 615
1
vote
1
answer
70
views
Why is the polymorphic weight 1
I am reading through through a paper called HMF: Simple Type Inference for First-Class Polymorphism by Daan Leijen of Microsoft Research.
In the paper it describes how to calculate the polymorphic ...
- 121
8
votes
0
answers
95
views
Decidability of equality between higher-kinded equirecursive types (or: between nonregular Böhm trees)
In §3 of Polytypic values possess polykinded types, Ralf Hinze described a calculus of types with higher-kinded recursive types. There is a fixed-point combinator $$\mu_\kappa : (\kappa \rightarrow \...
- 161
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
3
votes
1
answer
171
views
What is contextual equivalence ignoring non-termination called?
Contextual equivalence ($M_1 \cong_{ctx} M_2$) is often defined as:
$C[M_1] \Downarrow V \iff C[M_2] \Downarrow V$
Which is to say for any context $C$, $C[M_1]$ terminates with value $V$ iff $C[M_2]$...
- 133
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
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
4
votes
1
answer
363
views
Resources for Church's paper "An Unsolvable Problem of Elementary Number Theory"?
I'm trying to understand and breakdown into simple English Church's paper for "An Unsolvable Problem of Elementary Number Theory" but I'm not finding anything useful online, only citations and links ...
8
votes
2
answers
865
views
How would a theory of computation course that culminated in lambda-calculus as "the" model of computation, instead of Turing machines, look like?
Currently, our ToC (Theory of Computation) courses are designed with the following progression of topics:
Finite automata and regular languages
Pushdown automata and context-free languages
Turing ...
- 5,255
4
votes
3
answers
655
views
Why is lambda calculus so "function" oriented?
I've always had this question nagging at me subconsciously but have never been able to intuitively grasp it. Why does $\lambda$-calculus have a functional notation? Why is everything a function?
It ...
- 5,255
8
votes
3
answers
1k
views
What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?
I've been reading Lectures on the Curry-Howard Isomorphism and it talks about intuitionistic/constructive logic (IL) , combinatory logic (CL) and lambda calculus ($\lambda$c) before moving on to the ...
- 5,255
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
6
votes
1
answer
138
views
In which posets is the set of compact elements downwards closed?
In a poset $(D, \sqsubseteq)$, a compact element is an element $d \in D$ such that for every directed set $A$ which happens to have a supremum $\bigsqcup A \in D$ with $d \sqsubseteq \bigsqcup A$, it ...
- 361
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
-1
votes
1
answer
259
views
How is does a scheme lambda function relate to lambda calculus?
For example:
(define fact
(lambda (n)
(if (< n 2) 1 (* n (fact (- n 1)))))
How is this an example of applied lambda calculus? I tried to read the ...
- 111
10
votes
3
answers
585
views
Is there any known CCC closed under a probabilistic powerdomain operation?
Equivalently, is there a known denotational semantics for probabilistic higher-order functional programming languages? Specifically, is there a domain model of pure untyped $\lambda$-calculus extended ...
- 265
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,911
3
votes
2
answers
593
views
Constructing terms of function types out of the empty type
If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we ...
- 505
5
votes
1
answer
353
views
Commutativity of addition in polymorphic lambda calculus
In the article "Extensional models of polymorphism" by Breazu-Tannen and Coquand, natural numbers are presented using a Church-like encoding:
$polyint = \forall t . (t \to t) \to t \to t$
Addition ...
- 195
8
votes
1
answer
333
views
Church-Rosser equivalent for concatenative languages?
Looking at the striking parallels between combinatory logic and concatenative languages makes me wonder how many theorems of the former hold in the latter. The Church-Rosser theorem is particularly ...
- 181
0
votes
0
answers
173
views
Is there an algorithm to find whether 2 combinators form a Turing-complete system?
It is known that K = (λx.(λy.x)) and S = (λx.(λy.(λz.((x z) (y z))))) define a turing complete system, and we know procedures to ...
- 3,117
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
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
7
votes
1
answer
2k
views
Are there presentations of set theory in terms of lambda-calculus?
I am planning to implement in software a set theory language, based on a binary function, which in set theory is the so called adjunction operation: $f(x, y) = x \cup$ {y}. Therefore, a presentation ...
- 71
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
12
votes
1
answer
876
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
5
votes
1
answer
572
views
Is this behavior in a programming language inconsistent?
I'm developing a tiny programming language to try to wrap my head around type inference, and I'm trying to figure out if its behavior makes sense or not. Here's the problem:
The identity function <...
- 153
6
votes
1
answer
133
views
A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2
I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's Lambda calculi with types (1992), a chapter in Handbook in logic in computer science. (I'm referring to the PostScript version available ...
- 895
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
7
votes
1
answer
360
views
Are there stronger notions of equivalence over lambda terms than beta equivalence?
I should add the context that I am concerned with strongly normalizing systems like System-F.
I have what I consider a very strong notion of equivalence for lambda terms that goes something like the ...
- 1,141
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
7
votes
1
answer
183
views
Upper bound on Chaitin's constant for lambda calculus and SKI combinatory logic
I'd like to have proof that Chaitin's constant for lambda calculus and/or SKI combinatory logic is pretty small. I've found some approximations (accurate to about 63 binary digits) for truing machines ...
- 1,141
2
votes
2
answers
371
views
How to translate general recursion into a set of $\mu$-recursive operator applications?
I'm trying to find a scheme to translate a functional language with let rec into a set of primitives called "generalized arrows", i.e. $\kappa$-calculus with ...
- 203
8
votes
2
answers
565
views
Can factorial be encoded in the Kappa-calculus with fixed point operator?
Suppose we have a $\kappa$-calculus with operator $fix$, that could be used to transform function with type $(1 \rightarrow a) \rightarrow a$ to a value of type $1 \rightarrow a$. We use a normal ...
- 203
11
votes
0
answers
304
views
A bijection between ordered lambda terms and rooted planar maps?
Consider the following recurrence in two parameters $n$ and $k$:
\begin{aligned}
NF(0,k) &= 0 \\
NF(n,k) &= Neu(n,k) + NF(n-1,k+1) \\
Neu(n,k) &= [n=1 \wedge k=1] + \sum_{l=1}^{n-1}\sum_{...
- 4,431
8
votes
0
answers
507
views
Complete combinator basis for System F-omega
The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
- 1,141
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
8
votes
0
answers
181
views
Equivalence of categories of directed complete posets
I asked this question there: https://math.stackexchange.com/questions/700975/equivalence-of-categories-of-directed-complete-posets.
Since I had no answer, I try here.
In the book ``Domains and Lambda-...
- 181