# Tagged Questions

**2**

votes

**2**answers

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

**3**

votes

**1**answer

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

**5**

votes

**2**answers

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

**1**

vote

**0**answers

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

**0**

votes

**1**answer

146 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

**0**answers

92 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

193 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\ |\ ...

**2**

votes

**0**answers

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

**1**

vote

**0**answers

62 views

### Optimal Reduction in Interaction Calculus

We work in interaction calculus.
Let $\Sigma = \{\lambda, \psi, \delta, \epsilon\}$, $\text{Ar}(\lambda) = \text{Ar}(\psi) = \text{Ar}(\delta) = 2$, and $\text{Ar}(\epsilon) = 0$.
For any $\alpha ...

**3**

votes

**2**answers

546 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

**1**answer

245 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

**1**answer

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

**5**

votes

**1**answer

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

**13**

votes

**3**answers

1k 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? ...