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
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
24
votes
0
answers
3k
views
What's the smallest $\lambda$-calculus term not known to have a normal form?
For Turing Machines, the question of halting behavior of small TMs has been well studied in the context of the Busy Beaver function, which maps n to the longest output or running time of any halting n ...
- 1,734
23
votes
1
answer
1k
views
What, mathematically speaking, does it mean to say that the continuation monad can simulate all monads?
In various places it is stated that the continuation monad can simulate all monads in some sense (see for example http://lambda1.jimpryor.net/manipulating_trees_with_monads/))
In particular, in http://...
- 639
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
20
votes
1
answer
2k
views
What is Chemlambda? In which ways could it be interesting for a mathematician?
I${}^{*}$ have randomly come across a couple of websites (Chemlambda project, chorasimilarity) that seem to be about a certain "thing" (a computer program, I think) called Chemlambda that does "stuff" ...
- 23.3k
19
votes
2
answers
1k
views
Do combinatory logic bases need a function of 3 variables?
All the known bases of combinatory logic, such as $\{S,K\}$, or $\{K,W,B,C\}$,
have one or more combinators using 3 variables:
\begin{align*}
S ={} & \lambda x\lambda y\lambda z. x z(y z), \\
B ={}...
- 1,734
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
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
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
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
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$...
- 765
12
votes
2
answers
3k
views
How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?
It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...
- 4,907
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
12
votes
2
answers
1k
views
Is there a proof of strong normalisation that uses ordinal numbers?
I am currently trying to find a proof for strong normalisation of an extension of $\lambda$-calculus.
I've tried several approaches and one would be to assign an ordinal number $\operatorname{cs}(t)$ ...
- 193
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. ...
12
votes
2
answers
929
views
An overview of mathematical-logical approaches in formalizing natural languages
Crossposted on Mathematics SE
I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach),...
11
votes
3
answers
1k
views
How to handle sums in Tait's reducibility proof of strong normalisation?
I've been reading Girard et al's 'Proofs and Types', which in Chapter 6 presents a proof of strong normalisation for the simply typed lambda calculus with products and base types. The proof is based ...
- 113
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
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
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
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
9
votes
2
answers
2k
views
Is simply typed lambda calculus with fixed-point combinator Turing-complete?
There are many sources cite that simply typed lambda calculus extended with fixed-point combinator is Turing complete. For example, Does there exist a Turing complete typed lambda calculus? or the ...
- 101
9
votes
0
answers
316
views
The geometry of lambda calculus?
I stumbled upon "the geometry of quantum computation" --- to quote the abstract:
Determining the quantum circuit complexity of a unitary operation is closely related to the problem of finding ...
- 1,221
9
votes
0
answers
539
views
The Curry Howard Isomorphism and models for an intuitionistic modal logic and its bimodal translation
My question regards the Curry Howard Isomorphism and how it constrains models in the case of a particular logic.
Consider quantified Lax Logic $QLL$.
https://pdfs.semanticscholar.org/468e/...
- 639
8
votes
1
answer
813
views
Easier Girard's paradox in a circular pure type system (PTS)
System U is an inconsistent PTS in that one has a term of type $\bot = \forall p\colon \ast \ldotp p$, and such a term is explicitly constructed in Hurkens' A Simplification of Girard's Paradox.
One-...
- 369
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
8
votes
1
answer
321
views
Is every total computable function definable by a normalizing lambda term?
$\newcommand{\nat}{\mathbb{N}}$
$\newcommand{\then}{\ \Longrightarrow\ }$
A partial function $f : \mathbb{N} \to \mathbb{N}$ is said to be $\lambda$-definable if there is a term $F \in \Lambda$ such ...
- 333
8
votes
0
answers
155
views
Is every total computable function definable by a strongly total lambda term?
Every computable (total) function $f : \mathbb{N} \to \mathbb{N}$ is definable in untyped pure lambda calculus in the sense that there is a term $F$ such that, for every Church's numeral $c_n = \...
- 4,459
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
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
7
votes
3
answers
2k
views
Relationship of lambda calculus to the rest of math
I just started reading "The calculi of lambda conversion" by Church.
Church defines functions like: id x = x, and says the domain and range are understood to be as permissible as possible. ...
- 181
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
7
votes
1
answer
183
views
Is lambda calculus polymorphism a type of generalized monad?
Let $\mathbf{C}$ be a Cartesian closed category. Then simply typed lambda calculus in $\mathbf{C}$ in one type variable can be interpreted as a category $\mathbf{STLC}_{\mathbf C}$ where the objects ...
7
votes
1
answer
375
views
Criterion for the consistency of pure type systems
Pure type systems are characterized in an almost combinatorial way: a set of axioms $\star_i : \star_j$, and a set of triples $(\star_i, \star_j, \star_k)$ saying when the dependent product $\prod_{x :...
- 1,262
7
votes
0
answers
181
views
CCCs, computational calculi and point-surjectivity
The models of some computational calculi are in a correspondence with Cartesian Closed Categories with an object $U$ that has some relationship to its exponential object $U^U$ e.g. a retraction ...
6
votes
1
answer
273
views
Consistency in pure type systems
Summary
My question is about how (i) a certain presentation of pure type systems in the $\lambda$-cube, bears on (ii) a standard definition of consistency in pure type systems. In short, I'm ...
- 63
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
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
5
votes
1
answer
264
views
Internal language proof of Lawvere's fixed point theorem for cartesian closed categories
This proof of Lawvere's fixed point theorem suggests (since it uses $\lambda$ notation) that it is written in the internal language of cartesian closed categories (which is the $\lambda$-calculus, as ...
- 723
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
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
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
95
views
$\omega$ incompleteness of $\lambda$ calculus
In Plotkin's 'The $\lambda$-Calculus is $\omega$-Incomplete' (The Journal of Symbolic Logic Vol. 39, No. 2 (Jun., 1974), pp. 313-317), an example is given of two (untyped) $\lambda$-terms $M$ and $N$ ...
- 358
4
votes
0
answers
114
views
Reflexive object and infinite products
The category CPO of cpos and continuous functions has a reflexive object, i.e. an object $A$ such that $A\times A\simeq A$ and $A\simeq A^A$. Since CPO has countable products, my question is whether ...
- 111
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
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
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 ...
- 19.7k
3
votes
1
answer
140
views
Where can I learn about Cartesian closed functors between categories of simply typed lambda calculus?
I'll try to describe the subject I am looking for literature on, or concept names that I can Google.
For each $n \geq 1$, let $\mathbf{STLC}_n$ be the category where the objects are all simply typed ...
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
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 ...