Co-routining

[User's Manual]
[Code]
SICStus Prolog follows a more complicated rule for computation than traditional implementations of Prolog. Instead of simply evaluating the leftmost rule in its search path, it evaluates the leftmost unblocked rule in its search path. This mechanism resembles co-routines in imperative programming languages, i.e., suspending and resuming different threads of control. SICStus Prolog provides some built-in co-routining predicates. These include:

• when(Condition,Goal): Block Goal until Condition is true, where Condition is a Prolog goal with the restricted syntax:

  nonvar(X)
  ground(X)
  ?=(X,Y)
  Condition,Condition
  Condition;Condition

• frozen/2
• dif/2
• call_residue/2

SICStus when/2 suspends a goal until (i) a variable is instantiated or (ii) two variables are equated or inequated. The latter case corresponds directly to structure-sharing and inequations in typed feature structures. The former, if it were to be carried over directly, would correspond to delaying until a variable was promoted to a type more specific than $\bot$. There are degrees of instantiation in the logic of typed feature structures, however, corresponding to subsumption chains that terminate in a most specific type. With signature in which this chain is of length more than two, a more general and useful primitive is then suspending until a variable is promoted to a particular type. ALE uses when_type(Type,X,Goal) to delay Goal until variable X reaches type Type.

To implement when_type(Type,X,Goal), we can actually use the underlying Prolog implementation of when/2. Types with no appropriate features constitute the base case, in which only delaying on the internal structure of the type's representation (which can be as simple as the type's name or a compound term encoding) is necessary. For types with appropriate features, we must ensure that our suspended Goal does not fire in between the time when the internal representation of a feature structure's type is updated, and when the appropriateness conditions for that type are enforced on the representation. To do otherwise would risk passing a non-well-typed or even non-well-formed representation in X to the delayed Goal. What when_type/3 must do is thus delay on the entire structure of the (well-typed) most general satisfier of its Type argument, relative to appropriateness and the type system, i.e., without considering any implicational constraints. That most general satisfier is guaranteed not to have any structure-sharing since appropriateness is not able to require this. As a result, only recursively delaying on the value restrictions of its appropriate features is necessary.