Search Results
| Search type | Search syntax |
|---|---|
| Tags | [tag] |
| Exact | "words here" |
| Author |
user:1234 user:me (yours) |
| Score |
score:3 (3+) score:0 (none) |
| Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
| Views | views:250 |
| Code | code:"if (foo != bar)" |
| Sections |
title:apples body:"apples oranges" |
| URL | url:"*.example.com" |
| Saves | in:saves |
| Status |
closed:yes duplicate:no migrated:no wiki:no |
| Types |
is:question is:answer |
| Exclude |
-[tag] -apples |
| For more details on advanced search visit our help page | |
Results tagged with lambda-calculus
Search options not deleted
user 22795
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.
1
vote
0
answers
134
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 Si …
3
votes
0
answers
263
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 t …
0
votes
Accepted
Hypothesis: interaction-based model for λKβη
One counterexample for the forward implication ($\not\Rightarrow$) is $M \equiv \lambda x.x\ I\ I$ and $M \equiv \lambda x.x\ I\ F$. Indeed,
$$
\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\ …
0
votes
Accepted
Turing-complete primitive blind automata
The construction is similar to that of Schönhage's Storage Modification Machine (SMM) model.
1
vote
0
answers
66
views
Posets with two partial (self-)distributive operations
Let $(X, {\sqsubset}, {\circ}, {\ast})$ be a set $X$ with a strict partial order $\sqsubset$ and two partial binary operations $\circ$ and $\ast$ such that for any $a, b, c \in X$:
$a \circ b$ and $ …
2
votes
Accepted
Universality of blind graph rewriting
The construction is similar to that of Schönhage's Storage Modification Machine (SMM) model.
2
votes
1
answer
286
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 exa …
3
votes
2
answers
789
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 functio …
1
vote
1
answer
222
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\ |\ x …
3
votes
0
answers
265
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 enco …
0
votes
Accepted
Interaction-based approximation for HP-complete λ-theory?
One counterexample for the forward implication ($\not\Rightarrow$) is solvable $M \equiv N \equiv \lambda x.x\ \Omega$. Indeed,
$$
\langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \not\r …
4
votes
1
answer
967
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 fr …
1
vote
0
answers
111
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 s …
1
vote
1
answer
169
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 …