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

66 questions
Filter by
Sorted by
Tagged with
61 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$ ...
915 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 ={}...
150 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 ...
1 vote
80 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 ...
99 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 ...
213 views

210 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. ...
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 ...
244 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 ...
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" ...
856 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://...
141 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$ ...
437 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/...
175 views

261 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 ...
670 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 ...
258 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 ...
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 ...
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. ...
216 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 ...
222 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 ...
514 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-...
548 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$...
313 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 ...
1 vote
92 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 ...
321 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 ...
566 views

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 $\... 9 votes 0 answers 241 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)$... 2 votes 2 answers 158 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 ... 4 votes 1 answer 262 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 ... 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 votes 3 answers 486 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$, ... 12 votes 1 answer 823 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? 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$-... 3 votes 1 answer 370 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$-... 1 vote 1 answer 164 views ### Interaction-based approximation for HP-complete λ-theory? We are looking for a proof or counter-examples for the following hypothesis. Two combinators$M$and$N$are solvable and equivalent in the HP-complete sensible$\lambda$-theory iff either$$\exists ... 1 vote 1 answer 197 views ### combinator SSS(SS)SS is not strongly normalizing. Why? I highly speculate that combinator SSS(SS)SS is not strongly normalizing. What is the argument for the non strong normalization? 1 vote 0 answers 104 views ### Schönhage's SMM with only one instruction It is possible to implement$\lambda$-calculus in Schönhage's storage modification machine using an infinite set of nodes and one single program consisted exclusively of (about hundred) instructions ... 1 vote 1 answer 214 views ### Hypothesis: interaction-based model for λKβη We are looking for a proof or counter-examples to the following Hypothesis. In interaction calculus$\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ ...
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 ...