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 al …

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 hun …

I highly speculate that combinator SSS(SS)SS is not strongly normalizing. What is the argument for the non strong normalization?

We are looking for counter-examples to the following Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnoth …

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. H …

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$. …

What is the recursive relation for H(m)=2^(m^2) using successor function recursive relation for multiplication: mult(x,0)=0; mult(x,S(y))=add(x,mult(x,y)) recursive relation for a …

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 node …

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 e …

In simple typed lambda calculus,are there any examples that the two closed subterms M and N are well typed but (M N) is not typeable?

Are there known compilations of the lambda calculus into interaction combinators other than that one by Mackie and Pinto in a same-name paper of 1998? We are interested in further …

Let us encode $λ$-expressions into interaction nets as with both abstraction and application nodes being interaction combinator $γ$. For sharing nodes, let us choose such an ag …

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 …

I have some background in set theory and automata and I am looking for a good place to start with lambda calculus.

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 v …