# 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.

81 questions
Filter by
Sorted by
Tagged with
123 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
87 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 ...
• 341
23 views

### For which categories can the Cartesian closedness of a category be described as a family of covariant functors?

The paper Functorial Polymorphism describes how parametric polymorphism can be described as dinatural transformations. It involves second order lambda calculus but my question is restricted to simply ...
183 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 ...
118 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
98 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
66 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 ...
156 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 ...
833 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
65 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 ...
159 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
56 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,272
84 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,484
102 views

• 1,091
1 vote
202 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
175 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 ...
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 ...
• 629
309 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,191
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,699
132 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 ...
• 173
104 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
66 views

• 21
151 views

• 765
322 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.5k
1 vote