WikiMili The Free Encyclopedia

**Interaction nets** are a graphical model of computation devised by Yves Lafont in 1990^{ [1] } as a generalisation of the proof structures of linear logic. An interaction net system is specified by a set of agent types and a set of interaction rules. Interaction nets are an inherently distributed model of computation in the sense that computations can take place simultaneously in many parts of an interaction net, and no synchronisation is needed. The latter is guaranteed by the strong confluence property of reduction in this model of computation. Thus interaction nets provide a natural language for massive parallelism. Interaction nets are at the heart of many implementations of the lambda calculus, such as efficient closed reduction^{ [2] } and optimal, in Lévy's sense, Lambdascope.^{ [3] }

Interactions nets are graph-like structures consisting of *agents* and *edges*.

An agent of type and with *arity* has one *principal port* and *auxiliary ports*. Any port can be connected to at most one edge. Ports that are not connected to any edge are called *free ports*. Free ports together form the *interface* of an interaction net. All agent types belong to a set called *signature*.

An interaction net that consists solely of edges is called a *wiring* and usually denoted as . A *tree* with its *root* is inductively defined either as an edge , or as an agent with its free principal port and its auxiliary ports connected to the roots of other trees .

Graphically, the primitive structures of interaction nets can be represented as follows:

When two agents are connected to each other with their principal ports, they form an *active pair*. For active pairs one can introduce *interaction rules* which describe how the active pair rewrites to another interaction net. An interaction net with no active pairs is said to be in *normal form*. A signature (with defined on it) along with a set of interaction rules defined for agents together constitute an *interaction system*.

Textual representation of interaction nets is called the *interaction calculus*^{ [4] } and can be seen as a programming language.

Inductively defined trees correspond to *terms* in the interaction calculus, where is called a *name*.

Any interaction net can be redrawn using the previously defined wiring and tree primitives as follows:

which in the interaction calculus corresponds to a *configuration*

,

where , , and are arbitrary terms. The ordered sequence in the left-hand side is called an *interface*, while the right-hand side contains an unordered multiset of *equations*. Wiring translates to names, and each name has to occur exactly twice in a configuration.

Just like in the -calculus, the interaction calculus has the notions of *-conversion* and *substitution* naturally defined on configurations. Specifically, both occurrences of any name can be replaced with a new name if the latter does not occur in a given configuration. Configurations are considered equivalent up to -conversion. In turn, substitution is the result of replacing the name in a term with another term if has exactly one occurrence in the term .

Any interaction rule can be graphically represented as follows:

where , and the interaction net on the right-hand side is redrawn using the wiring and tree primitives in order to translate into the interaction calculus as using Lafont's notation.

The interaction calculus defines reduction on configurations in more details than seen from graph rewriting defined on interaction nets. Namely, if , the following reduction:

is called *interaction*. When one of equations has the form of , *indirection* can be applied resulting in substitution of the other occurrence of the name in some term :

or .

An equation is called a *deadlock* if has occurrence in term . Generally only deadlock-free interaction nets are considered. Together, interaction and indirection define the reduction relation on configurations. The fact that configuration reduces to its *normal form* with no equations left is denoted as .

Interaction nets benefit from the following properties:

**locality**(only active pairs can be rewritten);**linearity**(each interaction rule can be applied in constant time);**strong confluence**also known as one-step diamond property (if and , then and for some ).

These properties together allow massive parallelism.

One of the simplest interaction systems that can simulate any other interaction system is that of *interaction combinators*.^{ [5] } Its signature is with and . Interaction rules for these agents are:

- called
*erasing*; - called
*duplication*; - and called
*annihilation*.

Graphically, the erasing and duplication rules can be represented as follows:

with an example of a non-terminating interaction net that reduces to itself. Its infinite reduction sequence starting from the corresponding configuration in the interaction calculus is as follows:

Interaction nets are essentially deterministic and cannot model non-deterministic computations directly. In order to express non-deterministic choice, interaction nets need to be extended. In fact, it is sufficient to introduce just one agent ^{ [6] } with two principal ports and the following interaction rules:

This distinguished agent represents ambiguous choice and can be used to simulate any other agent with arbitrary number of principal ports. For instance, it allows to define a boolean operation that returns true if any of its arguments is true, independently of the computation taking place in the other arguments.

In mathematics, a **differential operator** is an operator defined as a function of the differentiation operator. It is helpful, as a matter of notation first, to consider differentiation as an abstract operation that accepts a function and returns another function.

In the calculus of variations, a field of mathematical analysis, the **functional derivative** relates a change in a functional to a change in a function on which the functional depends.

In mathematics, the **Hodge star operator** or **Hodge star** is a linear map defined on the exterior algebra of a finite-dimensional oriented vector space endowed with a nondegenerate symmetric bilinear form. The result when applied to an element of the algebra is called the element's **Hodge dual**. This map was introduced by W. V. D. Hodge.

In physics, the **S-matrix** or **scattering matrix** relates the initial state and the final state of a physical system undergoing a scattering process. It is used in quantum mechanics, scattering theory and quantum field theory (QFT).

In differential geometry, a **tensor density** or **relative tensor** is a generalization of the tensor field concept. A tensor density transforms as a tensor field when passing from one coordinate system to another, except that it is additionally multiplied or *weighted* by a power *W* of the Jacobian determinant of the coordinate transition function or its absolute value. A distinction is made among (authentic) tensor densities, pseudotensor densities, even tensor densities and odd tensor densities. Sometimes tensor densities with a negative weight *W* are called **tensor capacity.** A tensor density can also be regarded as a section of the tensor product of a tensor bundle with a density bundle.

In electromagnetism, the **electromagnetic tensor** or **electromagnetic field tensor** is a mathematical object that describes the electromagnetic field in spacetime. The field tensor was first used after the four-dimensional tensor formulation of special relativity was introduced by Hermann Minkowski. The tensor allows related physical laws to be written very concisely.

In general relativity, the **Gibbons–Hawking–York boundary term** is a term that needs to be added to the Einstein–Hilbert action when the underlying spacetime manifold has a boundary.

In mathematics, a **compact quantum group** is an abstract structure on a unital separable C*-algebra axiomatized from those that exist on the commutative C*-algebra of "continuous complex-valued functions" on a compact quantum group.

The **time-evolving block decimation** (**TEBD**) algorithm is a numerical scheme used to simulate one-dimensional quantum many-body systems, characterized by at most nearest-neighbour interactions. It is dubbed Time-evolving Block Decimation because it dynamically identifies the relevant low-dimensional Hilbert subspaces of an exponentially larger original Hilbert space. The algorithm, based on the Matrix Product States formalism, is highly efficient when the amount of entanglement in the system is limited, a requirement fulfilled by a large class of quantum many-body systems in one dimension.

In Riemannian geometry, the **Gauss–Codazzi–Mainardi equations** are fundamental equations in the theory of embedded hypersurfaces in a Euclidean space, and more generally submanifolds of Riemannian manifolds. They also have applications for embedded hypersurfaces of pseudo-Riemannian manifolds.

The **KeY** tool is used in formal verification of Java programs. It accepts specifications written in the Java Modeling Language to Java source files. These are transformed into theorems of dynamic logic and then compared against program semantics that are likewise defined in terms of dynamic logic. KeY is significantly powerful in that it supports both interactive and fully automated correctness proofs. Failed proof attempts can be used for a more efficient debugging or verification-based testing. There have been several extensions to KeY in order to apply it to the verification of C programs or hybrid systems. KeY is jointly developed by Karlsruhe Institute of Technology, Germany; Technische Universität Darmstadt, Germany; and Chalmers University of Technology in Gothenburg, Sweden and is licensed under the GPL.

In Riemannian geometry, **Gauss's lemma** asserts that any sufficiently small sphere centered at a point in a Riemannian manifold is perpendicular to every geodesic through the point. More formally, let *M* be a Riemannian manifold, equipped with its Levi-Civita connection, and *p* a point of *M*. The exponential map is a mapping from the tangent space at *p* to *M*:

**Range concatenation grammar** (RCG) is a grammar formalism developed by Pierre Boullier in 1998 as an attempt to characterize a number of phenomena of natural language, such as Chinese numbers and German word order scrambling, which are outside the bounds of the Mildly context-sensitive languages.

The **calculus of moving surfaces** (**CMS**) is an extension of the classical tensor calculus to deforming manifolds. Central to the CMS is the Tensorial Time Derivative whose original definition was put forth by Jacques Hadamard. It plays the role analogous to that of the covariant derivative on differential manifolds. in that it produces a tensor when applied to a tensor.

In quantum field theory, and especially in quantum electrodynamics, the interacting theory leads to infinite quantities that have to be absorbed in a renormalization procedure, in order to be able to predict measurable quantities. The renormalization scheme can depend on the type of particles that are being considered. For particles that can travel asymptotically large distances, or for low energy processes, the **on-shell scheme**, also known as the physical scheme, is appropriate. If these conditions are not fulfilled, one can turn to other schemes, like the Minimal subtraction scheme.

The **Maxwell–Bloch equations**, also called the **optical Bloch equations**, were first derived by Tito Arecchi and Rodolfo Bonifacio of Milan, Italy. They describe the dynamics of a two-state quantum system interacting with the electromagnetic mode of an optical resonator. They are analogous to the Bloch equations which describe the motion of the nuclear magnetic moment in an electromagnetic field. The equations can be derived either semiclassically or with the field fully quantized when certain approximations are made.

**Computable topology** is a discipline in mathematics that studies the topological and algebraic structure of computation. Computable topology is not to be confused with algorithmic or *computational topology*, which studies the application of computation to topology.

**Vasiliev equations** are *formally* consistent gauge invariant nonlinear equations whose linearization over a specific vacuum solution describes free massless higher-spin fields on anti-de Sitter space. The Vasiliev equations are classical equations and no Lagrangian is known that starts from canonical two-derivative Frønsdal Lagrangian and is completed by interactions terms. There is a number of variations of Vasiliev equations that work in three, four and arbitrary number of space-time dimensions. Vasiliev's equations admit supersymmetric extensions with any number of super-symmetries and allow for Yang-Mills gaugings. Vasiliev's equations are background independent, the simplest exact solution being anti-de Sitter space. It is important to note that locality is not properly implemented and the equations give a solution of certain formal deformation procedure, which is difficult to map to field theory language. The higher-spin AdS/CFT correspondence is reviewed in Higher-spin theory article.

In theoretical physics, the **dual graviton** is a hypothetical elementary particle that is a dual of the graviton under electric-magnetic duality predicted by some formulations of supergravity in eleven dimensions.

This article summarizes important identities in exterior calculus.

- ↑ Lafont, Yves (1990). "Interaction nets".
*Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*. ACM: 95–108. doi:10.1145/96709.96718. ISBN 0897913434. - ↑ Mackie, Ian (2008). "An Interaction Net Implementation of Closed Reduction".
*Implementation and Application of Functional Languages: 20th International Symposium*. Lecture Notes in Computer Science.**5836**: 43–59. doi:10.1007/978-3-642-24452-0_3. ISBN 978-3-642-24451-3. - ↑ van Oostrom, Vincent; van de Looij, Kees-Jan; Zwitserlood, Marijn (2010). "Lambdascope: Another optimal implementation of the lambda-calculus" (PDF).Cite journal requires
`|journal=`

(help) - ↑ Fernández, Maribel; Mackie, Ian (1999). "A calculus for interaction nets".
*Principles and Practice of Declarative Programming*. Lecture Notes in Computer Science. Springer.**1702**: 170–187. doi:10.1007/10704567. ISBN 978-3-540-66540-3. - ↑ Lafont, Yves (1997). "Interaction Combinators".
*Information and Computation*. Academic Press, Inc.**137**(1): 69–101. doi:10.1006/inco.1997.2643. - ↑ Fernández, Maribel; Khalil, Lionel (2003). "Interaction Nets with McCarthy's Amb: Properties and Applications".
*Nordic Journal of Computing*.**10**(2): 134–162.

- Asperti, Andrea; Guerrini, Stefano (1998).
*The Optimal Implementation of Functional Programming Languages*. Cambridge Tracts in Theoretical Computer Science.**45**. Cambridge University Press. ISBN 9780521621120. - Fernández, Maribel (2009). "Interaction-Based Models of Computation".
*Models of Computation: An Introduction to Computability Theory*. Springer Science & Business Media. pp. 107–130. ISBN 9781848824348.

- de Falco, Marc. "tikz-inet. A set of tikz-based macros for drawing interaction nets".
- de Falco, Marc. "INL. Interaction Nets Laboratory".
- Vilaça, Miguel. "INblobs. An editor and interpreter for Interaction Nets".
- Asperti, Andrea. "The Bologna Optimal Higher-Order Machine".
- Salikhmetov, Anton. "JavaScript Engine for Interaction Nets".
- Salikhmetov, Anton. "Macro Lambda Calculus".

This page is based on this Wikipedia article

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.

Text is available under the CC BY-SA 4.0 license; additional terms may apply.

Images, videos and audio are available under their respective licenses.