Skip to main content

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.

Filter by
Sorted by
Tagged with
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 ...
Steffen Jensen's user avatar
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 ...
John Tromp's user avatar
  • 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://...
user65526's user avatar
  • 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 ...
beroal's user avatar
  • 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" ...
Qfwfq's user avatar
  • 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 ={}...
John Tromp's user avatar
  • 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 ...
Tom LaGatta's user avatar
  • 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? ...
Dan Ramras's user avatar
  • 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 ...
Marcus Booster's user avatar
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}$...
winitzki's user avatar
  • 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$...
StudentType's user avatar
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 ...
Mike Battaglia's user avatar
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.
user16132's user avatar
  • 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)$ ...
Zermelo-Fraenkel's user avatar
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),...
Heleyrine Brookvinth's user avatar
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 ...
RAC's user avatar
  • 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 ...
darij grinberg's user avatar
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?
Alexey Muranov's user avatar
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 ...
Keith's user avatar
  • 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?...
Charles Stewart's user avatar
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 ...
kittyphon's user avatar
  • 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 ...
Siddharth Bhat's user avatar
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/...
user65526's user avatar
  • 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-...
H Koba's user avatar
  • 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$, ...
Wolfgang Jeltsch's user avatar
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 ...
Andrew Polonsky's user avatar
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 = \...
Valery Isaev's user avatar
  • 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)$ ...
fritzo's user avatar
  • 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 $\...
Matthew's user avatar
  • 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. ...
Polymer's user avatar
  • 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)\...
kow's user avatar
  • 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 ...
Johan Thiborg-Ericson's user avatar
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 :...
Trebor's user avatar
  • 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 ...
alessio-b-zak's user avatar
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 ...
Spaceka13's user avatar
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 $\...
meditans's user avatar
  • 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 ...
meditans's user avatar
  • 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 ...
user1005113's user avatar
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 ...
Andrew Bacon's user avatar
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 ...
Bob's user avatar
  • 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$ ...
provocateur's user avatar
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 ...
Steve K.'s user avatar
  • 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 ...
mshang's user avatar
  • 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 ...
Hans-Peter Stricker's user avatar
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 ...
James Propp's user avatar
  • 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 ...
Johan Thiborg-Ericson's user avatar
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$-...
Alfie's user avatar
  • 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 ...