The tag has no wiki summary.

learn more… | top users | synonyms

5
votes
3answers
405 views

Exponentials in the opposite category of finite separable algebras

Let $K$ be a field and $G=Gal(K_s/K)$ is its absolute Galois group. Then, by Galois theory, the category of finite separable algebras over $K$ (denoted by $Sep(K)$) and the category of finite ...
0
votes
1answer
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
1answer
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
0answers
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
0answers
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 ...
1
vote
0answers
108 views

Turing-complete primitive interaction systems

Let us call primitive an interaction system with the signature $\Sigma = \{(\rho, 0), (\xi, n)\}, \quad n \geq 2;$ and the only rule being of the form $\rho \bowtie \xi[\rho, \xi(a_1, \dots , a_n), ...
7
votes
1answer
326 views

Looking for papers and articles on the Tarskian Möglichkeit

Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator: $\Diamond A =_{def} \neg A \to A$ (which he ...
14
votes
1answer
657 views

How is Fredkin and Toffoli's Conservative Logic related to Linear Logic?

In the answers to this question, Timothy Gowers asks: I've been interested in this question for some time. I haven't put any serious thought into it, so all I can offer is a further question ...
3
votes
3answers
338 views

What is the proper name for “compact closed” multiplicative intuitionistic linear logic?

Multiplicative intuitionistic linear logic (MILL) has only multiplicative conjunction $\otimes$ and linear implication $\multimap$ as connectives. It has models in symmetric monoidal closed ...