Interaction Combinators

@article{Lafont1997InteractionC,
  title={Interaction Combinators},
  author={Yves Lafont},
  journal={Inf. Comput.},
  year={1997},
  volume={137},
  pages={69-101},
  url={https://api.semanticscholar.org/CorpusID:16385844}
}
It is shown that a very simple system ofinteraction combinators, with only three symbols and six rules, is a universal model of distributed computation, in a sense that will be made precise. This…
View via Publisher
core.ac.uk
95 Citations
Highly Influential Citations
19
Background Citations
44
Methods Citations
17
Results Citations
3

Figures from this paper

95 Citations

Edifices and Full Abstraction for the Symmetric Interaction Combinators

It is proved that two nets are observationally equivalent iff they have the same edifice, and Edifices may be compared to Bohm trees in infinite η-normal form, or to Nakajima trees, and give a precise topological account of phenomena like infiniteη-expansion.

Full Abstraction for Set-Based Models of the Symmetric Interaction Combinators

The problem of full abstraction with respect to one of observational equivalences for symmetric interaction combinators is studied, using a class of very simple denotational models based on pointed sets.

A denotational semantics for the symmetric interaction combinators

A denotational semantics is introduced for the symmetric interaction combinators, which is inspired by the relational semantics for linear logic, and an injectivity and full completeness result is proved for it.

Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators

    Damiano Mazza
    Computer Science, Mathematics
    Log. Methods Comput. Sci.
  • 2009
A full abstraction result is obtained by interpreting nets as certain subsets of the Cantor space, called edifices, which play the same role as Boehm trees in the theory of the lambda-calculus.

Encoding Linear Logic with Interaction Combinators

The purpose of this paper is to demonstrate how Lafont's interaction combinators, a system of three symbols and six interaction rules, can be used to encode linear logic. Specifically, we give a…

Bounded Combinatory Logic and lower complexity

Interaction Nets and Concurrency

It is shown that Interaction Nets with Multiple Principal Ports (INMPP) are a very expressive model of concurrent computation by encoding within them the -calculus (without sums or match).

Observational Equivalence for the Interaction Combinators and Internal Separation

Hard combinators

Universal Hard Interaction for Clockless Computation

The universality of natural subclasses of hard systems and the main ideas that lead to a universal system with 7 rules called Hard Combinators are highlighted.
...

12 References

Combinators for Interaction Nets

    S. Gay
    Mathematics, Computer Science
    Theory and Formal Methods
  • 1994
A set of combinators which is complete in the sense of being able to encode all possible patterns of interaction in Lafont's Interaction Nets, a graph rewriting system based on classical linear logic.

An algorithm for optimal lambda calculus reduction

We present an algorithm for lambda expression reduction that avoids any copying that could later cause duplication of work. It is optimal in the sense defined by Lévy. The basis of the algorithm is a…

The geometry of optimal lambda reduction

This paper connects and explains the geometry of interaction and Lamping's graphs, which offer a new understanding of computation, as well as ideas for efficient and correct implementations.

Connection graphs

This paper presents connection graph grammars as an abstract model for parallel computation and shows how this model helps to modularize the programming language problem into two pieces.

Geometry of Interaction 1: Interpretation of System F

Linear logic without boxes

An implementation of proof nets without boxes is described, which helps in understanding optimal reductions in the lambda -calculus and in the various programming languages inspired by linear logic.

Linear logic: its syntax and semantics

The first objection to that view is that there are in mathematics, in real life, cases where reaction does not exist or can be neglected : think of a lemma which is forever true, or of a Mr. Soros, who has almost an infinite amount of dollars.

From proof-nets to interaction nets

Proof-nets and the Hilbert space

Interaction nets

A new kind of programming language, with the following features: a simple graph rewriting semantics, a complete symmetry between constructors and destructors, and a type discipline for deterministic and deadlock-free (microscopic) parallelism.