Co-routining

[Reference Manual]
[Code--compiling conditionals] [Code--coroutining primitives]
Co-routining allows programmers to block the execution of a particular thread of execution until some event is witnessed. In logic programming, variables serve as the witnesses to these events -- naturally extending their role as representatives of state in the logical setting. Users who are already familiar with SICStus Prolog's when/2 should exercise some caution with ALE's own when/2 predicate: as described in further detail below, its conditional expressions generalize SICStus Prolog's conditional expressions to the typed case in such a way that a condition may provably never occur, and its treatment of shared variables in conditional expressions is also necessarily different (see Section 5.2.1). Unlike SICStus Prolog, ALE currently provides no support for residuation or examination of blocked goals.

when/2 delays execution until some event is witnessed. This is often used to protect very declaratively written goals from non-termination in certain calling contexts, or to make highly disjunctive goals more efficient, by waiting until a condition is observed that reduces the number of satisfying disjuncts. A common example is:

foo(X) :-
  ...                 % NewVar does not occur here
  when((X=ne_list;X=e_list),append(X,List,NewVar)).

append([],L,L) if true.
append([H|T],L,[H|Res]) if
  append(T,L,Res).

The call to when/2 in foo/1 waits until X is either a non-empty list or an empty list before calling append/3. Not to do so with the definition of append/3 given above, that is, calling append/3 when X is only of type list or bot, would result in an infinite number of possible answers, because NewVar is a new variable. A more compact way of writing the same thing is:

foo(X) :-
  ...         % NewVar does not occur here
  when((X=max(list),append(X,List,NewVar)).

This waits until X has one of the maximally specific types that list subsumes. In general, this method is to be preferred because ALE can implement it more efficiently, but there are some disjunctive conditionals that cannot be re-expressed in this fashion without declaring extra types in the signature.

The first argument to when/2 is called a conditional expression or block condition; it expresses the event that ALE must wait for before executing the goal in the second argument to when/2. Fundamentally, conditional expressions take the form of equations in which the left-hand side is an ALE variable (denoting a typed feature structure), and the right-hand side is a function-free, inequation-free description. Macros can be used, as long as the macros do not expand to a description that contains a function or an inequation. Conditional expressions are closed under conjunction and disjunction, both at the description-level inside the right-hand side of a conditional equation, and outside at the level of the conditional equations themselves. The example above uses an ``outside'' disjunction, which could have been expressed ``inside'' as:

foo(X) :-
  ...                 % NewVar does not occur here
  when(X=(ne_list;e_list),append(X,List,NewVar)).

Neither is more efficient than the other, but ``outside'' disjunctions must be used when the left-hand side variables differ.

When ALE encounters a goal blocked by a conditional equation, it waits until the equation is known to be necessarily true or false. This typically happens as a result of the program or grammar acquiring more information about a variable, such as the structure-sharing of two of its features' values, or a more specific or join-compatible type. If the conditional equation becomes provably false, i.e., if it becomes known that it will never be true, then the blocked goal is discarded and never executed. If it becomes true, then the blocked goal is executed. If independently blocked goals have the same conditional, or have conditionals that become provably true at the same time, then it is unpredictable in which order they will be executed. If any blocked goal fails, then execution fails back to the point where the goal was blocked, not executed. For the most part, this is in keeping with the operational behaviour of when/2 in SICStus Prolog.

Unlike SICStus Prolog conditionals such as nonvar/1 or ?=/2, however, an ALE conditional expression may become provably false. A conditional equation on a type, for example, such as X=e_list, can never become true once X promotes to an incompatible type, such as ne_list. Blocked goals in ALE should be written with this fact in mind. In particular, Prolog goals blocked on ?=/2 in SICstus Prolog must check for equality or inequality because ?=/2 could become true by virtue of either, whereas ALE goals blocked on structure-sharing are executed only as a result of equality. ALE goals cannot be blocked on inequality.

The BNF syntax for conditionals is given in the appendix.

Shared variables in conditionals

Particular care must also be taken with shared variables in ALE conditional expressions because there are two scopes within which they can be quantified. The goal:

when(X=([f]==[g]),bar(X))

for example, is not the same as:

when(X=(f:Y,g:Y),bar(X))

because the former waits until the F and G values of X are equal, whereas the latter waits until the F and G values of X are both equal to the value of some variable Y. Variables such as Y are quantified with scope over the entire clause within which the when/2 statement occurs, just as any other body variable in ALE or Prolog. Unlike Prolog, however, ALE provides the ability to change this quantification to take narrower scope in block conditions. The goal

when(Y^(X=(f:Y,g:Y)),bar(X))

is equivalent to a delay on a path equation between F and G, as in the first alternative above. It waits until there exists a Y such that both the F and G values are equal to it. Y is called a narrowly quantified variable, and its scope is the when/2 statement in which it occurs. When baz/2 is called by this clause, for example:

foo(X) :-
  Z = f:Y,
  when(Y^(X=(f:Y,g:Y)),baz(Y,Z)).

the first occurrence of Y is not necessarily the same as the F and G values of X (which are both equal to the first argument of baz/2). The first occurrence of Z, on the other hand, is the same as the second argument of baz/2.

The left-hand side variable of a conditional equation may not be a narrowly quantified variable with scope over the same when/2 goal. In other words, this goal:

when(X^(X=f:t),foo(Y))

is not allowed, whereas this goal:

when(X^(Y=f:(t,X)),when(X=g:t,foo(Y)))

is allowed. X can occur on the left-hand side of the blocked when/2 goal because it was narrowly quantified in a different when/2 goal.