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
1
vote
0
answers
122
views
How could I formally express: System F cannot express universal quantification over things that are not types? [closed]
I'm trying to understand exactly why it is that https://ncatlab.org/nlab/show/computational+trilogy states that quantification requires dependent types, and why this wouldn't be possible to achieve ...
- 113
2
votes
1
answer
119
views
Do free variables play a significant role in the Busy Beaver for Lambda Calculus?
I happened to stumble upon this sequence. It defines the function $BB_{\lambda}(n)$, which is the maximum normal form size of any closed lambda term of size $n$.
However, I noticed this sequence only ...
- 23
2
votes
1
answer
140
views
Does substitution on named terms correspond to substitution on de Bruijn terms?
Altenkirch wrote (in the unpublished draft α-conversion is easy):
I leave it to the reader to show that (some natural translation function) preserves substitution, i.e. it maps substitutions on named ...
1
vote
1
answer
98
views
Selection terms in the untyped lambda calculus
In the untyped $\lambda$-calculus, are there terms $S$ and $T$ such that for any $n$ and any terms $t_1, \dotsc, t_n$,
$$S(T(t_1)\dots(t_n)) \twoheadrightarrow_{\beta} t_1$$
Of course, if $n$ is fixed ...
- 358
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
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 ...
1
vote
0
answers
102
views
Can application in untyped lambda calculus be seen as the uncurried unit of some monad?
Simply typed lambda calculus in one type variable in a Cartesian closed category $\mathbf{C}$ can be interpreted as a family of Cartesian closed functors (described below, do they have a name?) from ...
1
vote
0
answers
67
views
Does lambda polymorphism have some universal property?
To evaluate some typed lambda calculus applications, the type of the function might have to be "lifted" in order to match the type of the value it is applied to. For example, in the ...
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 ...
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),...
1
vote
0
answers
66
views
Second order lambda calculus as dinatural transformations in some category of CCCs
Let $\textbf{CART}$ be a category where the objects are all Cartesian closed categories (henceforth shortened as CCC). Is there any way to define the arrows so that $\textbf{CART}$ itself becomes ...
2
votes
1
answer
171
views
Semiring axioms which almost implement inverse, searching for domains other than lambda calculus
I'm working with an idempotent semiring which contains elements $C_i, \hat{C_i}$ with the following properties:
$$ {C}_i \hat{C_j} = 0 \quad\text{where}\quad i \neq j \quad\quad\quad\quad(\beta_0)$$
$$...
- 225
1
vote
0
answers
62
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$...
- 1,382
0
votes
0
answers
93
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 ...
- 2,624
3
votes
0
answers
122
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)(\...
- 193
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
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
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
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
1
vote
0
answers
97
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 ...
- 73
3
votes
0
answers
206
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 ...
- 1,263
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,263
1
vote
0
answers
219
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 ...
- 482
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 ...
0
votes
0
answers
110
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 ...
- 639
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
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
3
votes
0
answers
138
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 ...
- 353
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
1
vote
0
answers
66
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 ...
2
votes
0
answers
288
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. ...
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
3
votes
0
answers
264
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 ...
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
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
3
votes
0
answers
147
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$ ...
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
2
votes
0
answers
183
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 \...
- 21
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
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
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
2
votes
1
answer
327
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 ...
- 31
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
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
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
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 ...
- 765
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
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
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
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 ...