entailment

0 The first algorithm

One algorithm to test $x == y$ is as follows. For $x$ and $y$, construct a graph where the nodes represent variables in the store, and an edge from feature $i$ of a record variable $a$ to a variable $b$ represents the fact that $a.i$ is $b$.

If the graphs are structurally similar, then $x == y$.

1 Algorithm

The following algorithm may also work to compute the entailment operator. This algorithm does not test for structural similarity of graphs - instead, it tries to mimic the unification algorithm in its steps except that it does not introduce any new bindings.

The following algorithm is used for computing whether $x==y$ where $x$ and $y$ are variables.

1.1 $x==y$

If the pair $(x,y)$ is marked as being tested, then entailment evaluates to true. (This is to handle recursive calls to the same pair.)
If $(x,y)$ are not marked as being tested, then execute the first case of the following, that applies.
If $x$ and $y$ are the same variable (i.e. the entailment is $x==x$), then the entailment evaluates to true.
Unbound Variables
1. If $x$ and $y$ are unbound but belong to different equivalence classes, then entailment suspends.
2. If $x$ and $y$ are unbound variables equivalent to each other, then entailment evaluates to true.
3. If exactly one variable is bound and the other unbound, then entailment suspends.
$x$ bound to a number
1. If $x$ is bound to a number $n_1$ and $y$ is bound to a number $n_2$, then entailment evaluates to true if $n_1$ is the same as $n_2$ and to false otherwise.
2. If $x$ is bound to a number and $y$ is bound to a record or a procedure, then entailment evaluates to false.
$x$ bound to a procedure
1. If $x$ is bound to a procedure or $y$ is bound to a procedure or both are bound to procedures, then entailment evaluates to false. (Note: This is slightly different in the full-blown Oz implementation you usually run: see the Example 1.)
$x$ bound to a record $label(f_1:x_1 \dots f_k:x_k)$
1. If $y$ is bound to a number or a procedure, then entailment evaluates to false.
2. If $y$ is a record with a different label or a different arity (i.e. feature set), then entailment evaluates to false.
3. If any of $x_1 \backslash= y_1$ or $x_2 \backslash= y_2$ or $\dots$ or $x_k \backslash= y_k$ holds, then entailment evaluates to false. This case can apply even when some of these terms cause entailment to suspend. This can be done even in a sequential interpreter, and clearly can be done if we can test these terms in parallel.
4. If $(x_1 == y_1) \land (x_2 == y_2) \land \dots \land (x_k == y_k)$, then entailment evaluates to true.
5. If none of these subcases apply, then entailment suspends.

Finally, unmark the pair $(x,y)$ and return the evaluation of the entaiment.

2 Example 1

declare F G H
F = proc {$ ?X} X=1 end
G = F
H = proc {$ ?X} X=1 end
{Browse F==G} % true
{Browse F==H} % false

3 Example 2

local X in
  X = 1|X
  {Browse X==1|X}
end

Then we see if $X.1 == (1|X).1$ and if $X.2 == (1|X).2$.

$X.1$ is 1 and $(1|X).1$ is 1, so the first entailment evaluates to true.

$X.2$ is $X$, and $(1|X).2$ is true as well.

4 Example 3

local X in
  X = 1|X
  {Browse X==1|(1|X)}
end

This reduces to

First, $X.1 == 1$ This evaluates to true.

Second, $X.2 == (1|X).2$, i.e. $X == (1|X)$, which we analyzed to be true in the previous example.

5 Example 4

local X Y in
  X = 1|Y
  Y = 1|X
  {Browse X==Y}
end

$X == Y$ reduces to $X.1 == Y.1$ , that is, $1==1$, and $X.2 == Y.2$, that is, $Y==X$. Since $(X,Y)$ are marked as being tested at the beginning of the call, the second test will return true. Thus, the whole entailment returns true.

6 Example 5

local X Y Z in
  X = 1|Y
  Y = 1|Z
  Z = 1|X
  X==Y
end

X==Y reduces to Y==Z, which reduces to Z==X, which in turn reduces to X==Y. Hence the entailment evaluates to true.