Questions tagged [lambda-calculus]
For questions on the formal system in mathematical logic for expressing effective functions, programs and computation, and proofs, using abstract notions of functions and combining them through binding and substitution.
82 questions
6
votes
1
answer
359
views
On an automatic translation of typed lambda calculus in untyped lambda calculus
I have a question regarding the "compilation" of typed lambda calculus in untyped lambda calculus.
Take for example the inductive definition of lists, with introduction rules:
and:
We can ...
- 243
6
votes
1
answer
737
views
Explanation of the definition of Saturated Sets in Lambda Calculus
I have a question on the definition of Saturated Sets, as particular subset of the set of strongly normalizing terms in lambda calculus.
Here is the definition: a set $S$ of strongly normalizing $\...
- 243
8
votes
0
answers
248
views
Is there a notion analogous to separability but requiring definable rather than countable sets?
Among models of $\lambda$-calculus, some like the Bohm tree model have the property that every element is a directed sup of definable elements, whereas others like the $D_\infty$ and $P(\omega)$ ...
- 211
2
votes
2
answers
181
views
Background for Kierstead terms
I was looking at some slides of John Longley's here, where he mentions "the Kierstead functional"
$$\lambda f.f(\lambda x.f(\lambda y.x)) \ ,$$
(where $f$ should be of type $2$, and $x,y$ of ground ...
- 269
4
votes
1
answer
278
views
internal language for the 2-category of small categories
What is the internal language of the category Cat of small categories?
I found an article by Glynn Winskel and his student Mario Jose Cáccamo about such calculus! However it is limited to a fragment ...
- 476
18
votes
3
answers
1k
views
Example of a space for which $V \cong Hom(V,V)$
Let $V$ be a topological linear space, and let $\operatorname{Hom}(V,V)$ be the space of continuous linear maps from $V$ back to $V$, equipped with a suitable topology.
Is there a non-trivial ...
- 8,512
8
votes
3
answers
662
views
Models of intuitionistic linear logic that reflect the resource interpretation
I am interested in models of intuitionistic linear logic, that is, the logic that you get if you take classical linear logic and restrict the set of operators to $\otimes$, $1$, $\multimap$, $\times$, ...
- 951
11
votes
1
answer
979
views
Why did Alonzo Church choose the letter $\lambda$ as the "binding operator"?
Is there any known reason why Alonzo Church chose Greek $\lambda$ as the "binding operator" for the Lambda Calculus?
- 1,481
16
votes
2
answers
3k
views
Why is there no product type in simply typed lambda-calculus?
$\DeclareMathOperator\Pair{Pair}\DeclareMathOperator\First{First}\DeclareMathOperator\Second{Second}\DeclareMathOperator\Left{Left}\DeclareMathOperator\Right{Right}\DeclareMathOperator\Choice{Choice}$...
- 271
3
votes
1
answer
404
views
Is there an easy decision algorithm for the inhabitation problem for simple types?
Consider the basic system of simple types usually known as $TA_\lambda$. One can prove that (as a consequence of the Subject Reduction Property and the fact that any typable term is strongly $\beta$-...
- 31
1
vote
1
answer
169
views
Interaction-based approximation for HP-complete λ-theory?
We are looking for a proof or counter-examples for the following hypothesis.
Two combinators $M$ and $N$ are solvable and equivalent in the HP-complete sensible $\lambda$-theory iff either
$$
\exists ...
1
vote
1
answer
314
views
combinator SSS(SS)SS is not strongly normalizing. Why?
I highly speculate that combinator SSS(SS)SS is not strongly normalizing. What is the argument for the non strong normalization?
1
vote
0
answers
111
views
Schönhage's SMM with only one instruction
It is possible to implement $\lambda$-calculus in Schönhage's storage modification machine using an infinite set of nodes and one single program consisted exclusively of (about hundred) instructions ...
1
vote
1
answer
223
views
Hypothesis: interaction-based model for λKβη
We are looking for a proof or counter-examples to the following
Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ ...
3
votes
0
answers
266
views
Is it possible to implement η-reduction in interaction nets?
There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. However, all the ...
3
votes
2
answers
790
views
Turing-complete primitive blind automata
Let $N$ be the set of natural numbers, $S$ be the set of finite binary sequences, and
$Q = [N \rightarrow N] \times [N \rightarrow N],$
where $[N \rightarrow N]$ is the set of all computable ...
2
votes
1
answer
286
views
Universality of blind graph rewriting
Let us consider $S(M) = \{(f_0, f_1) | f_0, f_1: M \rightarrow M\}$, where $M$ is a finite set. Each element of $S(M)$ is equivalent to a finite directed
graph with the set of nodes $M$, which has ...
4
votes
1
answer
967
views
Algebraic structure generated by primitive graph operations
Let $M$ be a finite set, and
$S(M) = \{(f_0, f_1) | f_0, f_1: M → M\}$.
Each element of $S(M)$ can be considered as a finite directed graph with the set of nodes $M$, which has exactly two arrows ...
4
votes
0
answers
635
views
Difference between lambda-calculus with well-formed formulas vs properly-formed formulas
In S.C. Kleene's 1935 paper "$\lambda$-definability and recursiveness," he proves that all $\lambda$-definable functions are general recursive in the Herbrand-Godel sense and vice-versa. However, the ...
- 141
12
votes
7
answers
17k
views
What is some good introduction to lambda calculus?
I have some background in set theory and automata and I am looking for a good place to start with lambda calculus.
- 131
11
votes
4
answers
1k
views
Why is alpha-equivalence in untyped $\lambda$-calculus substitutive?
This is something all introductory texts seem to avoid proving, and many even avoid stating.
We consider untyped $\lambda$-terms on some countably infinite alphabet. If $x$ is a variable and $p$ is ...
- 33.8k
7
votes
1
answer
531
views
Are innermost reductions perpetual in untyped $\lambda$-calculus?
Background
In the untyped lambda calculus, a term may contain many redexes, and
different choices about which one to reduce may produce wildly
different results (e.g. $(\lambda x.y)((\lambda x.xx)\...
- 461
0
votes
1
answer
429
views
Is it correct to state that basic primitive recursive functions are in fact combinators?
Is it correct saying that the Zero, Successor and Projection functions can be seen as combinators?
- 103
24
votes
6
answers
39k
views
Difference between a 'calculus' and an 'algebra'
What is really the conceptual difference between a calculus and an algebra.
Eg. Is SKI combinator calculus really a calculus?
A friend claims that free variables are fundamental for a calculus, and ...
- 267
17
votes
3
answers
3k
views
What is the history of the Y-combinator?
Inspired by the comments to this question, I wonder if someone can explain the history of the fixed point combinator (often called the Y combinator) in lambda calculus.
Where did it first appear? ...
- 8,803
20
votes
5
answers
3k
views
[solved] sequent calculus as programming language
intuitionistic logic ~ programming
natural deduction ~ lambda-calculus
Hilbert system ~ combinatory logic {S, K}
Gentzen system=sequent calculus ~ ?
What would you write in place of the question ...
- 530
7
votes
4
answers
1k
views
What is the intuitive meaning of star and box in a pure type system?
The systems of the λ-cube have the axiom $\star:\square$.
I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\...
- 303
10
votes
2
answers
2k
views
Scott on the consistency of the lambda calculus
I have twice heard it attributed to Dana Scott that he said something to the effect that the consistency of the lambda-calculus was an accident.
Does anyone have a reasonable-sounding source for this?...
- 2,283
11
votes
4
answers
2k
views
Can dependent sums be encoded as dependent products?
Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...
- 211
12
votes
3
answers
7k
views
Is functional programming a branch of mathematics?
In Theory mainly concerned with lambda-calculus?, F. G. Dorais wrote, of the idea that the lambda-calulus defines a domain of mathematics:
That would never stick unless there's another good reason. ...
3
votes
5
answers
2k
views
Theory mainly concerned with $\lambda$-calculus?
Automata theory is mainly concerned with Turing machines and all its relatives-in-spirit. $\lambda$-calculus is rather rarely mentioned in textbooks on automata theory.
What's the common name of the ...
- 9,720
16
votes
7
answers
3k
views
What is lambda calculus related to?
So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based.
I was wondering if anyone had a suggestion ...
- 163