Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

6
votes
2answers
401 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 ...
0
votes
0answers
17 views

Semi universal proper combinator

It is known that the two combinators S and K defined by Sxyz=xz(yz), Kxy=x, generate all other possible combinators. It is also known that no single proper combinator (combinator that can be defined ...
3
votes
0answers
230 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 ...
13
votes
1answer
783 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" ...
21
votes
1answer
591 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://...
3
votes
0answers
117 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$ ...
8
votes
0answers
308 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/...
2
votes
0answers
128 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 \...
8
votes
0answers
118 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 = \...
8
votes
1answer
164 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 ...
7
votes
3answers
296 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 ...
3
votes
1answer
169 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 ...
5
votes
2answers
688 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 ...
7
votes
3answers
574 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. ...
5
votes
0answers
192 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 ...
3
votes
0answers
184 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 ...
6
votes
1answer
289 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-...
14
votes
1answer
460 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$...
3
votes
2answers
304 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
0answers
78 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 ...
6
votes
1answer
249 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 ...
3
votes
1answer
362 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 $\...
9
votes
0answers
235 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
2answers
143 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
1answer
214 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
3answers
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 ...
6
votes
3answers
390 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$, ...
11
votes
1answer
632 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?
11
votes
2answers
2k 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
1answer
304 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
1answer
159 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
1answer
164 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
0answers
101 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
1answer
208 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\ |\ ...
4
votes
0answers
211 views

Is it possible to implement η-reduction in interaction nets?

There are several ways to encode λ-terms in interaction nets; for instance, using the original optimal algorithm by Lamping, or compiling λ-calculus into interaction combinators. However, all the ...
3
votes
2answers
722 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 ...
0
votes
1answer
264 views

Universality of blind graph rewriting

Let us consider $S(M) = \{(f_0, f_1) | f_0, f_1: M \rightarrow M\}$, where $M$ is a finite set. Each element of $S(M)$ is equivalent to a finite directed graph with the set of nodes $M$, which has ...
3
votes
1answer
939 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
0answers
496 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 ...
9
votes
7answers
9k 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.
8
votes
4answers
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 ...
6
votes
1answer
425 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)\...
0
votes
1answer
346 views

Is it correct to state that basic primitive recursive functions are in fact combinators?

Is it correct saying that the Zero, Successor and Projection functions can be seen as combinators?
23
votes
6answers
35k 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 ...
18
votes
3answers
2k 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? ...
13
votes
5answers
2k 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 ...
6
votes
4answers
826 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 $\...
7
votes
2answers
1k 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?...
8
votes
4answers
1k 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 ...
12
votes
3answers
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. ...