Clauses may use ‘`state variables`’ as a shorthand for naming
intermediate values in a sequence. That is, where in the plain syntax one
might write

main(IO0, IO) :- io.write_string("The answer is ", IO0, IO1), io.write_int(calculate_answer(…), IO1, IO2), io.nl(IO3, IO).

using state variable syntax one could write

main(!IO) :- io.write_string("The answer is ", !IO), io.write_int(calculate_answer(…), !IO), io.nl(!IO).

A state variable is written ‘`!. X`’ or ‘

Within each clause, a transformation converts state variables into
sequences of ordinary logic variables. The syntactic conversion is
described in terms of the notional ‘`transform`’ function defined
next.

The transformation is applied once for each state variable `X`
with some fresh variables which we shall call `ThisX` and `NextX`.

The expression
‘`substitute( Term, X, ThisX, NextX)`’
stands for a copy of

State variables obey special scope rules.
A state variable `X` must be explicitly introduced either in the head of
the clause or lambda (in which case it may appear as either or both of
‘`!. X`’ or ‘

For instance, the following clause employing a lambda expression

p(A,B, !S) :- F = (pred(C::in,D::out) is det :- q(C,D, !S) ), ( F(A,E) ->B=E;B=A).

is illegal because
it implicitly refers to ‘`!: S`’ inside the lambda expression.
However

p(A,B, !S) :- F = (pred(C::in,D::out, !.S::in, !:S::out) is det :- q(C,D, !S) ), ( F(A,E, !S) ->B=E;B=A).

is acceptable because the state variable `S` accessed
inside the lambda expression is locally scoped to the lambda expression
(shadowing the state variable of the same name outside the lambda expression),
and the lambda expression may refer to
the next version of a local state variable.

There are three restrictions concerning state variables in lambdas: first,
‘`! X`’ is not a legitimate function result, since it stands for two
arguments, rather than one; second, ‘

`Head`:-`Body`transform((

`Head`:-`Body`),`X`,`ThisX`,`NextX`) = substitute(`Head`,`X`,`ThisX`,`NextX`) :- transform(`Body`,`X`,`ThisX`,`NextX`)`Head`-->`Body`transform((

`Head`-->`Body`),`X`,`ThisX`,`NextX`) = substitute(`Head`,`X`,`ThisX`,`NextX`) :- transform(`Body`,`X`,`ThisX`,`NextX`)`Goal1`,`Goal2`transform((

`Goal1`,`Goal2`),`X`,`ThisX`,`NextX`) = transform(`Goal1`,`X`,`ThisX`,`TmpX`), transform(`Goal2`,`X`,`TmpX`,`NextX`)for some fresh variable

`TmpX`.`Goal1`;`Goal2`transform((

`Goal1`;`Goal2`),`X`,`ThisX`,`NextX`) = transform(`Goal1`,`X`,`ThisX`,`NextX`) ; transform(`Goal2`,`X`,`ThisX`,`NextX`)`not`

`Goal``\+`

`Goal`A negation. The two different syntaxes have identical semantics.

transform((not

`Goal`),`X`,`ThisX`,`NextX`) = not transform(`Goal1`,`X`,`ThisX`,`DummyX`),`NextX`=`ThisX`for some fresh variable

`DummyX`.`if`

`Goal1`then`Goal2`else`Goal3``Goal1`->`Goal2`;`Goal3`An if-then-else. The two different syntaxes have identical semantics.

transform((if

`Goal1`then`Goal2`else`Goal3`),`X`,`ThisX`,`NextX`) = if transform(`Goal1`,`X`,`ThisX`,`TmpX`) then transform(`Goal2`,`X`,`TmpX`,`NextX`) else transform(`Goal3`,`X`,`ThisX`,`NextX`)for some fresh variable

`TmpX`.`Goal1`=>`Goal2``Goal2`<=`Goal1`An implication. The two different syntaxes have identical semantics.

transform((

`Goal1`=>`Goal2`),`X`,`ThisX`,`NextX`) = transform(`Goal1`,`X`,`ThisX`,`TmpX`) => transform(`Goal2`,`X`,`TmpX`,`NextX`),`NextX`=`ThisX`for some fresh variable

`TmpX`.`all`

`Vars``Goal`transform((all

`Vars``Goal`),`X`,`ThisX`,`NextX`) = all`Vars`transform(`Goal`,`X`,`ThisX`,`DummyX`),`NextX`=`ThisX`for some fresh variable

`DummyX`.`some`

`Vars``Goal`transform((some

`Vars``Goal`),`X`,`ThisX`,`NextX`) = some`Vars`transform(`Goal`,`X`,`ThisX`,`NextX`)`!`

`X`^`field_list`:=`Term`A field update. Replaces a field in the argument.

`Term`must be a valid data-term.`field_list`must be a valid field list. See Record syntax.transform((!

`X`^`field_list`:=`Term`),`X`,`ThisX`,`NextX`) = NextX = ThisX ^ field_list := Term`Call_or_Unification`If ‘

`!:`’ does not appear in`X``Call_or_Unification`thentransform(

`Call_or_Unification`,`X`,`ThisX`,`NextX`) = substitute(`Call_or_Unification`,`X`,`ThisX`,`NextX`),`NextX`=`ThisX`If ‘

`!:`’ does appear in`X``Call_or_Unification`thentransform(

`Call_or_Unification`,`X`,`ThisX`,`NextX`) = substitute(`Call_or_Unification`,`X`,`ThisX`,`NextX`)

This transformation can lead to the introduction of chains of unifications for variables that do not otherwise play a role in the definition. Such chains are removed transparently.

The following code fragments illustrate appropriate use of state variable syntax.

**Threading the I/O state**main(!IO) :- io.write_string("The 100th prime is ", !IO), X = prime(100), io.write_int(X, !IO), io.nl(!IO).

**Handling accumulators (1)**foldl2(_, [], !A, !B). foldl2(P, [X | Xs], !A, !B) :- P(X, !A, !B), foldl2(P, Xs, !A, !B).

**Handling accumulators (2)**iterate_while2(P, F, !A, !B) :- ( if P(!.A, !.B) then F(!A, !B), iterate_while2(P, F, !A, !B) else true ).