As of May 31, 2023, we have updated our Code of Conduct.

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
1 vote
0 answers
31 views

The set of closed untyped $\lambda$-terms is not context-free?

The set of untyped $\lambda$-terms is obviously context-free. But, according to Barendregt's paper Discriminating coded lambda terms (six lines before Theorem 1.5), the set of closed untyped $\lambda$...
Paul Blain Levy's user avatar
0 votes
0 answers
20 views

Can second order lambda calculus in a category C be seen as a mixed variance functor from C and the category of lambda calculus to C?

$\DeclareMathOperator\MC{MC}\DeclareMathOperator\LAM{LAM}$Let $\mathbf{L}$ be the category of simply typed lambda calculus, where the objects are all signatures for lambda calculus, and the arrows are ...
Johan Thiborg-Ericson's user avatar
0 votes
0 answers
80 views

Can the Haskell kind system be interpreted as a category?

Background I consider myself fairly knowledgeable about the parts of category theory that concerns computer science, and while I have seen many examples of how Haskell kind constructors can be thought ...
Johan Thiborg-Ericson's user avatar
0 votes
0 answers
69 views

Univalence and higher inductive types in the lambda calculus model of type theory

In appendix A1 of the homotopy type theory book by the Univalent Foundations Project, the authors give a formal presentation of Martin-Löf type theory in lambda calculus. However, they did not give ...
Madeleine Birchfield's user avatar
3 votes
0 answers
87 views

When does weak normalization imply strong normalization?

Is there a possibility to get strong normalization for some kind of $\lambda$-calculus out of weak normalization with some other assumptions? For example: The term $(\lambda_y z)((\lambda_x xx)(\...
Zermelo-Fraenkel's user avatar
12 votes
2 answers
936 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
4 votes
0 answers
78 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
18 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,559
5 votes
1 answer
188 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
1 vote
0 answers
86 views

Is Set complete for the free CCC/lambda calculus over a monoidal signature?

To be precise, given a monoidal signature $S$ (i.e, a set of generating objects $O$ and morphisms with source and target taken in the free monoid over $O$) , we can generate the free Cartesian closed ...
FeralX's user avatar
  • 63
3 votes
0 answers
157 views

What is the connection between these proofs of strong normalization in $\lambda^\to$ and LK?

In Ralph Loader's lecture notes on lambda calculus (section 3.3), he states that a combinatorial proof of the SN of simply typed lambda calculus uses a technique that is "in essence that used by ...
Trebor's user avatar
  • 649
7 votes
1 answer
311 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
  • 649
1 vote
0 answers
168 views

What is the proof theoretic strength of PCF?

Godel's system $T$ means different, although equivalent, things to different people. To people working in the traditon of mathematical logic, $T$ is a quantifier-free equational theory of arithmetic ...
Not_Here's user avatar
  • 452
7 votes
0 answers
116 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
0 votes
0 answers
105 views

Expressing a model transformation by using monads in the simply-typed lambda calculus

In https://link.springer.com/content/pdf/10.1007/s10670-019-00128-z.pdf , page 16, the following clause is given for a modal operator $\langle R_k \rangle$ (see definition 4.2 for the definition of a ...
user65526's user avatar
  • 629
9 votes
0 answers
264 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
22 votes
0 answers
2k 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,559
3 votes
0 answers
118 views

When can all elements of $[A\to B]$ can be represented as computable functions?

(crosspost from math stackexchange) While working through Barendreght's book on the Lambda Calculus, and Abramsky's notes on Domain Theory, I had the following realization: It's often stated that ...
Alex Appel's user avatar
4 votes
0 answers
90 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
1 vote
0 answers
64 views

Posets with two partial (self-)distributive operations

Let $(X, {\sqsubset}, {\circ}, {\ast})$ be a set $X$ with a strict partial order $\sqsubset$ and two partial binary operations $\circ$ and $\ast$ such that for any $a, b, c \in X$: $a \circ b$ and $a ...
Anton Salikhmetov's user avatar
2 votes
0 answers
252 views

Lambda calculus as set-theoretic operations

It is possible to interpret typed lambda calculus a-la Church as logical operations (because of Curry-Howard correspondence). Also, there is a isomorphism between logical and set-theoretic operations. ...
семен антонов's user avatar
9 votes
2 answers
2k 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
3 votes
0 answers
250 views

Upward confluence in the interaction calculus

The lambda calculus is not upward confluent, counterexamples being known for a long time. Now, what about the interaction calculus? Specifically, I am looking for configurations $c_1$ and $c_2$ such ...
Anton Salikhmetov's user avatar
19 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
  • 22.2k
23 votes
1 answer
926 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
  • 629
3 votes
0 answers
145 views

One strong fixed-point property

Each topological space $A$ with fixed-point property is connected (all clopen subsets are trivial). This is an analog of Rice theorem (all decidable subsets are trivial). Suppose, we have a space $A$ ...
George Cherevichenko's user avatar
9 votes
0 answers
469 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
  • 629
2 votes
0 answers
181 views

Notation in 'The lambda calculus, its syntax and semantics' by H.P. Barendregt

I'm reading the book 'The lambda calculus its syntax and semantics'. In part 5, chapter 19: Local structure of Models, more specifically 19.2 Local structure of $D_\infty$, the notation $D_\infty \...
tpsp_lcs's user avatar
8 votes
0 answers
149 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,250
8 votes
1 answer
289 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
7 votes
3 answers
809 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
  • 73
3 votes
1 answer
286 views

Substructural types, the lambda calculus, and CCCs

It's well known that the simply-typed lambda calculus corresponds to a cartesian closed category. How would substructural type systems be characterized in category theory? For example, linear type ...
C. Bednarz's user avatar
8 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
7 votes
3 answers
1k 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
5 votes
0 answers
222 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
3 votes
0 answers
234 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 ...
StudentType's user avatar
7 votes
1 answer
619 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
  • 339
14 votes
1 answer
591 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
3 votes
2 answers
317 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
  • 18.8k
1 vote
0 answers
98 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 ...
Anton Salikhmetov's user avatar
6 votes
1 answer
341 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
  • 233
5 votes
1 answer
627 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
  • 233
9 votes
0 answers
244 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
  • 221
2 votes
2 answers
168 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 ...
Basil's user avatar
  • 269
4 votes
1 answer
270 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
  • 466
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,222
8 votes
3 answers
542 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
12 votes
1 answer
869 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
12 votes
2 answers
3k views

Why is there no product type in simply typed lambda-calculus?

Consider simply typed $\lambda$-calculus that has only the unit type as primitive. We would like to encode the product and the sum types. An encoding of the product type in the untyped $\lambda$-...
winitzki's user avatar
  • 231
3 votes
1 answer
380 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