127 lines
3.9 KiB
Markdown
127 lines
3.9 KiB
Markdown
---
|
|
title: "Interaction"
|
|
weight: 2
|
|
---
|
|
|
|
# Matchable rays
|
|
|
|
Usually, in the theory of term unification, we say that two terms (which are
|
|
basically rays without polarities) are *unifiable* where there a substitution
|
|
of variables making them equal. For instance `f(X)` and `f(h(Y))` are unifiable
|
|
with the substitution `{X:=h(Y)}` replacing `X` by `h(Y)`.
|
|
|
|
We are usually interested in the most general substitution. We could have
|
|
`{X:=h(c(a)); Y:={c(a)}` but it would be less general.
|
|
|
|
In the same fashion, we say that two rays are *matchable* when their underlying
|
|
terms (obtained by dropping polarities) are unifiable but we also want opposite
|
|
polarities to face each other instead of looking for equal symbols: we want
|
|
symbols prefixed with `+` to match same symbols but prefixed with `-`:
|
|
|
|
- `+f(X)` and `-f(h(a))` are matchable with `{X:=h(a)}`;
|
|
- `f(X)` and `f(h(a))` are not matchable;
|
|
- `+f(X)` and `+f(h(a))` are not matchable;
|
|
- `+f(+h(X))` and `-f(-h(a))` are matchable with `{X:=a}`;
|
|
- `+f(+h(X))` and `-f(-h(+a))` are matchable with `{X:=+a}`;
|
|
|
|
# Fusion
|
|
|
|
Stars are able to interact, through an operation called *fusion*, by using the
|
|
principle of Robinson's resolution rule. We define an operator `<i,j>` with
|
|
connects the `i`th ray of a star to the `j`th ray of another star.
|
|
|
|
Fusion is defined as follows for matchable rays `r` and `r'`:
|
|
```
|
|
r r1 ... rk <0,0> r' r1' ... rk' == theta(r1) ... theta(rk) theta(r1') ... theta(rk')
|
|
```
|
|
|
|
where `theta` is the most general substitution induced by `r` and `r'`.
|
|
|
|
Notice that:
|
|
- `r` and `r'` interact and are annihilated;
|
|
- the two stars are merged;
|
|
- the substitution resolving the conflict between `r` and `r'` is propagated to
|
|
adjacent rays.
|
|
|
|
For example:
|
|
```
|
|
X +f(X) <1,0> -f(a) == a
|
|
```
|
|
|
|
{{< hint info >}}
|
|
This corresponds to the cut rule for first-order logic except that we are
|
|
in a logic-agnostic setting (our symbols do not hold any meaning).
|
|
{{< /hint >}}
|
|
|
|
# Execution
|
|
|
|
You have to put a focus on some stars to start a computation as in:
|
|
```
|
|
X1, f(X1);
|
|
+a(X2 Y2);
|
|
@-h(f(X3 Y3)) +a(+f(X4) h(-f(X4)));
|
|
```
|
|
|
|
An *interaction configuration* is an expression `R |- I'` where:
|
|
- `R` is a static constellation called *reference constellation*. It corresponds
|
|
to unmarked stars;
|
|
- `I` is a dynamic constellation called *interaction space*. It corresponds to
|
|
all stars marked by a focus symbol `@`. It can be seen as a "working space".
|
|
|
|
The LSC execute constellations by looking for copies of partners in `R` for
|
|
each rays of `I`, as follows:
|
|
1. select a ray `ri` in a star `s` of `I`;
|
|
2. look for possible connections with rays `rj` belonging to stars in `R`;
|
|
3. duplicate `s` so that there is exactly one copy of `s` in `I` for every `rj`;
|
|
4. replace every copy by its fusion `s <i,j> s'`, where `s'` is the star to
|
|
which `rj` belongs;
|
|
5. repeat until there is no possible interaction in `I`.
|
|
|
|
The result of execution consists of all *neutral* stars that remain in `I`, i.e.
|
|
those without any polarized rays. Indeed, polarized stars are ignored/removed
|
|
because they correspond to *unfinished* (or stuck) computations.
|
|
|
|
# Example
|
|
|
|
We want to execute the following constellation:
|
|
```
|
|
+7(l:X) +7(r:X); 3(X) +8(l:X); @+8(r:X) 6(X);
|
|
-7(X) -8(X);
|
|
```
|
|
|
|
We distinguish an interaction space on which we focus interaction and a
|
|
reference constellation where we copy possible partners. We prefix `>>` for
|
|
selected rays. We have:
|
|
```
|
|
+7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) >>-8(X) |- >>+8(r:X) 6(X);
|
|
```
|
|
|
|
```
|
|
+7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- -7(r:X) 6(X);
|
|
```
|
|
|
|
```
|
|
+7(l:X) >>+7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- >>-7(r:X) 6(X);
|
|
```
|
|
|
|
```
|
|
+7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- +7(l:X) 6(X);
|
|
```
|
|
|
|
```
|
|
+7(l:X) +7(r:X); 3(X) +8(l:X); >>-7(X) -8(X) |- >>+7(l:X) 6(X);
|
|
```
|
|
|
|
```
|
|
+7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- -8(l:X) 6(X);
|
|
```
|
|
|
|
```
|
|
+7(l:X) +7(r:X); 3(X) >>+8(l:X); -7(X) -8(X) |- >>-8(l:X) 6(X);
|
|
```
|
|
|
|
```
|
|
+7(l:X) +7(r:X); 3(X) +8(l:X); -7(X) -8(X) |- 3(X) 6(X);
|
|
```
|
|
|
|
The result of the computation is `3(X) 6(X);`. |