next up previous

The off-line interpreter (specification)

The interpreter looks ahead up to the last choice point in each branch of the program (say, between alternative primitive actions), makes the choice and then proceeds backwards recursively, deciding at each choice point what branch is optimal.

A program begins with a deterministic action a.

tex2html_wrap_inline957


A program begins with the nondeterministic choice of two programs.
tex2html_wrap_inline957

Conditionals, recursive procedures and while loops can be specified as well.