
© Jørgen SteensgaardMadsen, Copenhagen, 2006

Statements



Statements are commonly known from several programming
languages. Examples are if and whilestatements. Conceptually these
are just applications of operations, but it may help to present them
in a traditional way.
Syntax overview
An operation signature associates a name with a list of
clause descriptions and possibly a result type. An application
of an operation is called a command.
Function arguments are simple examples of clauses, as are the branches
of a conditional command. In more complex cases a clause may be the
scope of some descendants of the command operation. Different
clauses will usually have different descendants. Saying clause
... is evaluated is short for computation expressed by
clause ... is performed.
A clause description is a signature itself: it associates a name
of the clause with a list of signatures of descendants.
Detailed information about the language of signatures and commands
will have to be found elsewhere.

[ if OF w
(Test:int)
[True:w]
[False:w] : w ]
w denotes the type of intended result.
Test is evaluated initially.
When the result is nonzero, the True clause is evaluated.
Otherwise, the False clause is evaluated.

[ when OF w
(condition:int)
[Body:w] ]
Like an ifstatement without a False clause

[ loop OF w
[Body ... : w]
: void ]
Iteration of the Body clause, see below.

[ while OF w
[Test:int]
[Body:w] ]
Repeatedly compute v by Test, and then Body,
until v is nonzero.

[ repeat OF w
[Body:w]
[Test:int] ]
Repeatedly compute Body and then v=Test until
v becomes zero

[ upto OF W
(n:int)
[Body ... : W]
: void ]
Compute Body upto n times, where n is the result of
computing n initially
Other statements may not be as familiar, but they certainly belong
in this category.

[ program OF W
[x:W] : W ]
A {...} that isn't a clause is treated as
program{...}, which an an operation is the
identity.

[ induction OF Problem,Result (Initial:Problem)
[Break_down ... : Result]
: Result ]
A statement form designed to emphasise a relation between
iteration and proofs by mathematical induction.
More below.

[ iterate OF Result,State
(S:State)
[Next ... : State] : Result ]
Iteration from an initial state towards a goal state. See below.

[ with OF V,W
(E:V)
[Body ... : W]
: W ]
Expression to compute
The named value is available in the Body clause only
Computes an expression and binds its value to a name.

[ accumulate ... ]
Obsolete.
Semantics
[ loop OF w[Body ... : w] : void ]
The computation of the Body clause is repeated until execution
of operation end, which has a signature (represented by the
ellipsis above):

[ end : void ]
Completes computation of the loop.
Note that a label may be associated with a Body clause:
loop A{ ... loop B{ ...; A.end; ... } ... }
where execution of A.end will cause the outer loop to terminate.
Semantics
[ upto OF W
(n:int)
[Body ... : W] : void ]
Signatures (...) of operations introduced in a Body clause are:

( i : int )
A count (0..n1) of previous executions of Body

( __ : int )
Default meaning of a label of Body  same as i

[ break : void ]
Causes (abnormal) termination of the iteration
Semantics
[ induction OF Problem,Result
(Initial:Problem)
[Break_down ... : Result] : Result ]
Use of induction can be as follows:
induction (L) P{ if (P==[],1,hd(P)*result(tl(P))) };
If L is a value of type int List the computation
finds the product of elements in L. The proof of this claim
goes as follows:
Let P be a list and P P the product of the elements of P.
By induction on the length of P we find
 If P is empty, P P is 1, as found by the computation.
 Otherwise, by assumption P tl(P)= result(tl(P)) is the product of elements of
tl(P), so the products of elements of P is
hd(P)*P tl(P), as found by the computation.
Thus we conclude that for any list of finite length
P L= induction (L) P{ if (P==[],1,hd(P)*result(tl(P))) }
Clause: Break_down of operation induction
Intended to tell how to solve a given problem under the assumption
that simpler problems can be solved by means of an auxiliary operation.
Semantics
[ iterate OF Result,State
(S:State)
[Next ... : State] : Result ]
Supports computations by sequences of states S_{0}, S_{1}, S_{2}, ... that
terminates and extracts a result from some final state S_{n}.
An example corresponding to the one for induction is
iterate((1,L)) X{if(snd(X)==[],fst(X),(fst(x)*hd(X),tl(X)))}
which may compute as follows: (1,[2,3,5]),(2,[3,5]),(6,[5]),(30,[])
and return 30.
Clause: Next of operation iterate
Intended to compute a next state S_{i+1} from S_{i}.
Semantics
[ with OF V,W
(E:V)
[Body ... : W] : W ]
Pattern of use is: { with(cpu_heavy(n)) x; ... xy ... }. It is
intended to avoid recomputation of intermediate results without resort
to mutable variables.
Clause: Body of operation with
Computes the final result using a name for the intermediate one.

( val : V )
Fixed name for the intermediate result

( __ : V )
Default meaning of a label of Body. Same as val.
Contents
File translated from
T_{E}X
by
T_{T}H,
version 3.33.
 On 18 Oct 2006, 16:47.

 