Draft Russian Translation: Interaction-Based Models of Computation

http://arxiv.org/abs/1304.1309

Interaction Nets in Russian

Draft translation to Russian of Chapter 7, Interaction-Based Models of Computation, from Models of Computation: An Introduction to Computability Theory by Maribel Fernandez. "In this chapter, we study interaction nets, a model of computation that can be seen as a representative of a class of models based on the notion of 'computation as interaction'. Interaction nets are a graphical model of computation devised by Yves Lafont in 1990 as a generalisation of the proof structures of linear logic. It can be seen as an abstract formalism, used to define algorithms and analyse their cost, or as a low-level language into which other programming languages can be compiled. This is fruitful because interaction nets can be implemented with reasonable efficiency."

η-редукция в сетях взаимодействия

http://mathoverflow.net/questions/126941/

Существуют несколько способов представить λ-термы в сетях взаимодействия; например, алгоритм Лэмпинга для оптимальной редукции или компиляция λ-исчисления в комбинаторы взаимодействия. Однако, все известные нам способы реализуют только β-редукцию, но не экстенсиональное λ-исчисление (где также есть η-редукция).

Можно ли представить λ-термы в сетях взаимодействия, реализовав βη-редукцию?

(Нормальная форма сети для терма должна соответствовать его βη-нормальной форме.)

Bisimilarity vs. Observational Equivalence

Operational equivalence for interaction nets
Maribel Fernández, Ian Mackie

The notion of contextual (or operational) equivalence is fundamental in the theory of programming languages. By setting up a notion of bisimilarity, and showing that it coincides with contextual equivalence, one obtains a simple coinductive proof technique for showing that two programs are equivalent in all contexts. In this paper we apply these (now standard) techniques to interactions nets, a graphical programming language characterized by local reduction. This work generalizes previous studies of operational equivalence in typed interaction nets since it can be applied to untyped systems, thus all systems of interaction nets are captured.

http://www.sciencedirect.com/science/article/pii/S0304397502006370

Observational Equivalence for the Interaction Combinators and Internal Separation
Damiano Mazza

We define an observational equivalence for Lafont's interaction combinators, which we prove to be the least discriminating non-trivial congruence on total nets (nets admitting a deadlock-free normal form) respecting reduction. More interestingly, this equivalence enjoys an internal separation property similar to that of Böhm's Theorem for the λ-calculus.

http://www.sciencedirect.com/science/article/pii/S1571066107001880