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`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`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`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 ).