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
5
votes
0
answers
228
views
Proper full submodels of full models of type theory
Let $N$ be the standard full model of the simply typed lambda calculus with infinite base type $o$ and let $X$ be an infinite and coinfinite subset of $N(o)$. I want to know if there's a full ...
- 357
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?
CommunityBot
- 1
3
votes
0
answers
283
views
Understanding Strong Normalization for Identity Types in Martin-Löf Intensional Type Theory [closed]
Roughly, the strong normalization property for Martin-Löf Intensional Type Theory (MITT) tells us that every closed term $t$ of type $M$ will eventually reach a canonical normal form $t’$ such that it ...
- 66.8k
14
votes
1
answer
641
views
Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?
Martin-Löf Extensional Type theory differs from its intensional counterpart in that it contains the so-called reflection rule that says that if $p : x = y$, then actually $x \equiv y$ (i.e. $x$ and $y$...
- 15.9k
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$, ...
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$-...
CommunityBot
- 1
3
votes
2
answers
327
views
Comparing really big numbers
Is there an intractability theorem that says that in any sufficiently rich system for defining really big numbers, there will be two numbers for which it's very, very, ... very difficult to decide ...
CommunityBot
- 1
1
vote
0
answers
137
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 ...
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 ...
- 1,452
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 $\...
- 1,452
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 ...
CommunityBot
- 1
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? ...
CommunityBot
- 1
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
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?
- 51
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 ...
- 201
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 ...
- 66.8k
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
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\ |\ ...
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 ...
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 ...
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 ...
CommunityBot
- 1
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 ...
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 ...
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 ...
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 ...
- 105
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
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 $\...
- 316
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)\...
CommunityBot
- 1
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
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 ...
- 2,283
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. ...
CommunityBot
- 1