FORMALIZATION OF RETURN ADDRESSES MANIPULATIONS AND CONTROL TRANSFERS
                             M.L.Gassanenko
                         St.Petersburg, Russia.
                              gml@ag.pu.ru

ABSTRACT

Unlike other programming languages, Forth enables the programmer to
access the return stack. This paper presents a calculus that describes
how return addresses manipulations are reflected in the control flow
changes.

The calculus is based on the notion of equivalence of code fragments and
enables one to analyse return addresses manipulations, prove their
correctness, perform equivalent transformations of code fragments
that manipulate with return addresses.

The approach to theory construction that was used introduces modularity
of theoretical knowledge.

1. THE BASING OF THEORY
1.1 FORMULATION OF THE PROBLEM

A Forth system is a two-stack engine: there is a data stack (holds data)
and a return stack, which holds return addresses. Access to return
addresses enables the programmer to implement both conventional
(described e.g. in [BaN88R]) and unconventional control structures of
Forth [Gas93R, Gas94, Cha91, Rod90b]. Return stack manipulations are
often used in text analysis [Cha91, Rod90a]. Techniques of return
addresses manipulations were in use from the very beginning of Forth,
but were never formally described and aren't allowed by the to-date ANSI
standard.

During the last 5 years theories of stack effects checking and
type inference were developed [Poi94 (review), Poi91, Poi93, StK92,
StK93, Sto93], but these formalisms do not address manipulations with
executable code addresses that are extremely important to Forth.

The fundamental difference between the data stack and the cotrol stack
manipulations lies in the fact that the return stack manipulations
may result in control transfers. For example, on a classical system
BRANCH my be defined as 

: BRANCH R> @ >R ;

The goals of this work are:

1) Description and analysis of the control flow changes due to
return addresses manipulations

2) Proof of correctness of return stack manipulations

3) Performing equivalent transformations of code fragments
that manipulate with return addresses

Another goal, which remains beyond the scope of this presentation, is
formal description of the implementation of backtracking [Gas94]. Formal
description of such untraditional aproach is a good test for a formal
model.

Mention should be made of Tuzov's works [Tuz88R, Tuz90R], where a
distinction between passive and active information was made. These works
describe a system where data first get transformed to executable form
and then execution of this code solves the problem.

Another important lesson was experience with BacFORTH [Gas93R, Gas94], a
system where more than 10 untraditional control structures were
implemented. Experience with self-modifying code [Gas93] also can be
mentioned.

1.2 THE APPROACH TO THEORY DEVELOPMENT

1) We want to construct a strict theory that, nevertheless, allowed
   to use common sense knowledge (which we understand as unformalized
   expert knowledge; doubtful pseudo-common-sense assertions may be
   recognized by an expert and are out of interest).

   a) We have to reconcile strict formal methods and unformal common
      sense

      (this is done by introducing a structure and putting them at
      different levels of knowledge).

   b) We have to develop a criterion to decide what is enough strict.

2) Why we have to use common sense (i.e. unformalized expert
   knowledge):

   a) Its use is often more effective in terms of time/cost

   b) It is a criterion of theory correctness.

   c) the mistakes made using formal methods can often be found by means of
      common sense (and vice versa).

3) Why use of common sense can be tolerated:

   a) expert knowlegde and judgements are not less reliable than formal
      methods (at least in some areas).

   b) we are not going to create theories that contradict common sense
      (i.e. expert knowledge).

   c) practice (e.g. physics, genetics) shows that it may be used.

4) Modularity of theoretical knowledge. We promote modular organization of
   theoretical knowledge, analogous to modular or object-oriented
   organization of program systems.

   a) Changes of description of the same phenomena become paintless.

      We may change the description of a phenomenon, and this will
      not affect other parts of theory that use its results.

   b) At the first stages of theory construction we can use intuitive
      notion and move later to a formal description.

   c) We have to discriminate between defined concepts and recognized
      concepts. To construct first defined concept in theory we
      normally use several recognized concepts. We cannot completely
      get rid of recognized concepts, although we prefer to use them
      only to create basic concepts.

   d) We have to discriminate between the utilization of a knowledge
      unit (a concept, a module (whatever it is), a theory) and the
      work at it.

      The term utilization ("primenenie") of a knowledge unit (e.g. a
      fact) implies that we do not use knowledge that explains why it
      is so. So, the term "utilization" stands for
      explanation-independent use. We can utilize different (but
      changeable) knowledge units in the same way.

      The term work at ("rabota s") the knowledge unit (e.g. the
      fact) implies that we do use internal knowledge that explains
      the fact. The term "work at" means explanation-dependent use.
      In the general case, we cannot work at different knowledge
      units (even if they are interchangeable) in the same way.

      A knowledge unit may include knowledge subunits, etc.

   e) Interchangeable approaches.

      A knowledge unit may be changed for another knowledge unit and
      this will not affect the knowledge units that utilize it.

   f) Concretization is not less important than abstraction.

      Concretisation is "deincapsulation" of knowledge, revealing the
      basing, the explanation. (An example of concretization is the
      use of unformal knowledge where formal methods do not work).

5) Virtual theorist as a means of knowledge incapsulation.

   a) We propose specifying a virtual theorist as the first step of
      theory construction.

      We specify what the theorist can do:

      1) the kwoledge units that the theorist utilizes;

      2) the knowledge units the theorist works at;

      3) the methods that the virtual theorist can use.

   b) It is impossible to start from nothing.

   c) The concept of "virtual theorist" allows to separate out the
      knowledge that will be considered elementary.

      The objects and operations that the theorist already knows are
      elementary and need no analysis.

   d) Specifying methods is important: answering the question "what
      can we do with it?" often eliminates the question "what is
      it?".


1.3. THE SUBJECT MATTER

1) The subject matter exists, it is not less real than e.g. a solid
   body. On the other hand, it is a result of utilization of what has
   been created by human beings (in contrast to machines that utilize
   physics laws). Therefore:

   a) we can use the natural sciences methods as well as formal ones;

   b) we do not need any experiments thus far since we can predict
      their results.

2) Known sorts of memory contents. The difference is in the ways of
   processing.

   We know 4 sorts of memory contents: executable code, data,
   self-modifying code and garbage. We will use the word
   "information" as a broad term referring to memory contents of any
   sort.

   The distinction between the different sorts of information is the
   way of processing.

   Garbage is what never gets used. (Probably, later one will find
   that it is more convenient to define garbage as what should never
   be used and to consider using gabage as an error).

   Executable code may be processed only by the code interpreter.

   Data may be processed in a variety of ways, except the code
   interpreter.

   Self-modifying and dynamically generated codes are processed
   alternately as code and as data.

   Only garbage and non-garbage differ fundamentally; there is no
   clear dividing line between code and data.

   It is possible that in some cases it will be convenient to
   introduce more sorts of information (e.g. code executed by the
   central processor and by an interpreter).

3) Eqivalence of threaded code fragments

   a) The criterion of equivalence of information fragments is
      equivalence of results of their processing by any method
      allowed for any of the fragments.

   b) Since different sorts of information assume different ways of
      processing, different concepts of equivalence should be applied
      to them. We can compare two information fragments for
      equivalence only if 1) they are processed by the same methods
      and 2) their results are processed in the same ways. Often it
      is not difficult to construct an aggregate method of processing
      both fragments (e.g. to compile a program by the appropriate
      compiler).

   c) Criteria of equivalence.

      From garbage nothing depends, therefore we can consider any
      combinations of bits as equivalent.

      The criterion of equivalence of code fragments is equivalence
      of their effects.

      The effect of code execution is twofold, it includes:
      1) output to the "outside world" and
      2) the state of computer memory.

      It seems reasonable to consider equivalent only identical
      outputs and ignore practical equivalence of such phrases as
      "strike any key when ready" and "press ENTER when done".

      To compare two states of memory, we have to know the methods of
      further processing.

      For the present we accept equality as the criterion of data
      equivalence. We ignore that data may be located at different
      addresses since all the languages can cope somehow with this
      problem.

4) The concept of position

   The use of word "position" reflects the fact that the way of
   processing is a feature rather of the context than of the
   information fragment itself.

   An information fragment may be in one of the following positions:

   a) active, if it is processed by nothing but the code interpreter;

   b) passive, if it is processed by anything but the code
      interpreter;

   c) blended, if it is processed by both the code interpreter and
      other methods;

   d) indifferent, if it is not processed at all.

   This set of notions describes the relations between an
   information fragment and the code interpreter well, but does not
   distinguish between other methods of processing. If we
   were interested in analysing other processing methods,
   we probably would have to introduce such notions for
   each of the processing methods.

   So, the code is in active position, data are in passive
   one, self-modifying and dynamically generated code are
   in blended position, and garbage is in indifferent
   position.

5) The modular approach and concordance with practice
   (common sense) enable us to move later to a more perfect
   definitions of equivalence and position.

6) Supposed internal structure of the Forth system

   a) The return address size is 1 cell, threaded code is located in
      the data address space.

   b) Compiler optimizations, if they are used, keep illusion of
      using threaded code.

   c) The threaded code access wordset:

   REF@ ( orig -- dest )   dest - is the address in [threaded] code,
                           pointed  to by the reference at orig.

   REF! ( dest orig -- )   set the reference at orig to point to
                           dest.

   REF+ ( orig -- addr )   addr is the address of threaded code that
                           follows the reference at orig.

   REF> ( orig -- addr dest ) dest is the threadded code address
                           pointed to by the reference at orig; addr
                           is the address of threaded code that
                           follows the reference at orig.

   TOKEN@ ( addr -- xt )   xt is the execution token of the word
                           compiled at addr.

   TOKEN! ( xt addr -- )   store the compilation token of the word
                           specified by the execution token xt to
                           addr.


   TOKEN+ ( addr -- addr' ) addr' is the address of threaded code
                           that follows the compilation token at
                           addr.

   TOKEN> ( addr -- addr' xt ) xt is the execution token of the word
                           compiled at addr; addr' is the address of
                           threaded code that follows the compilation
                           token at addr.

   The references are used in BRANCHes, etc. and may be of different
   nature in different systems (an address, a self-relative address,
   etc.)

   The term "compilation token" (or "compiled token") denotes the
   code that gets stored into dictionary when word gets compiled. The
   compiled tokens also may be of different nature in different
   systems.


1.4. THE FORMALISM

1) Equivalence of threaded code fragments is possibility to
   substitute one fragment by another. At the level of
   formalism only this fact is important, not its
   explanation.

   This may allow as to modify the definition of
   equivalence without breaking all the theory construction
   (if neither old nor new definitions and consequences
   contradict common sense).

2) We do not suppose that the Forth data stack exists. We
   only can or cannot state equivalence of two code
   fragments.


2. THE CALCULUS

2.1 THE TERMS AND THE NOTATION

We will say that a code fragment ignores something if it neither affect
nor depends upon it.

We will say that a code fragment is in active position if it can be
processed only by the code interpreter (and not by the functions that it
calls). The active position does not imply that the code gets
necessarily processed, or gets processed at all. The term "inactive
position" will be applied in cases when we do not state that something
is in active position. (Note that active position could be considered as
a particular case of inactive position, but we won't do it, since doing
so we disregard the only feature that enables us to analyse code).

Following the Forth tradition, the term "stack" will refer by default to
the data stack, while other stacks will be termed by their full names.

Abbreviations:

TC    -  threaded code
TCF   -  threaded code fragment

We will use the following latin letters to denote:

t..z      --- threaded code fragments (TCF);
f,g,h     --- functions (occupying exactly one threaded code element);
M,N       --- integer literals;
P,Q       --- properties (feaures);
i..n      --- natural numbers.

The meanings of separate signs:

[ and ] denote the boundaries of a TCF;
' -   address in active position;
^ -   address in passive position;
, -   a single threaded code element;
r -   mention of the return stack;
l -   mention of the L-stack (the stack of continuations [Gas94]);
: -   having a feature;
! -   assertion.

These signs are the elements from which all other symbols are
assembled. In the Forth language all they have a different meaning.

As in Forth, the symbols are separated by spaces.

Equivalence will be denoted by the symbol == and will be understood as
possibility to substitute one threaded code fragment for the other in
active position in any context. The symbol =/= will denote
inequivalence.

The =>= sign will be used in the cases where substitution is possible,
but some inormation gets lost:

   A =>= B

means that (probably, in view of some other statements)

   X == A  =>  X == B

(the => symbol denotes implication)

The notation

   x:P

may read as "x has the property P" or "x that has the property P". When
some properties are consequences of other properties, we will use the
symbol :! to underline that some properties refer to the consequence
rather than to the premise. For example, x:S2:!S1 is a concise notation
for x:S2 => x:S1 (translation: if a TCF ignores (neither affects nor
depends upon) two top data stack elements, it is also a fragmwnt that
ignores one top stack element).

When necessary, we will bracket the code fragment to which the property
applies. For example, [ x:R y:R ]:!R (translation: the code fragment
[ x y ], composed from two code fragments that ignore the return stack,
also ignores the return stack).

Now we give explanation of other symbols:

;              -  denotes EXIT

[r  x  ']  y   -  call of the threaded code fragment x with the
'r[  y  ]  x      continuation y; that is, place the address of y onto
                  the return stack and transfer control to x. The TCF y
                  is in active position.

[r  x  ^]  y   -  call of the threaded code fragment x with the
^r[  y  ]  x      continuation y; that is, place the address of y onto
                  the return stack and transfer control to x. The TCF y
                  is in inactive position.

'[  x  ]       -  place address of the threaded code fragment x, in
                  active position, onto the data stack.

^[  x  ]       -  place address of the threaded code fragment x, in
                  inactive position, onto the data stack.

,'[  x  ]      -  a threaded code element that contains a reference to a
                  TCF in active position.

,^[  x  ]      -  a threaded code element that contains a reference to a
                  TCF in inactive position.

,[  x  ]       -  the same as .'[  x  ]

^,^[  x  ]     -  the address of a threaded code element that contains a
                  reference to the TCF x in inactive position.

^,[  x  ]      -  the address of a threaded code element that contains a
^,'[  x  ]        reference to the TCF x in inactive position.

pre u  x       -  The TCF x is located in memory next to the TCF u.
 or
pre[ u ] x

,f             -  Compilation token of the function f (only one TC
                  element)

Act: x         -  The TCF x is in active position.

!Act: x        -  Assertion that x is in active position

%A             - universal quantifier

%E             - existential quantifier

We may change from "^" to "'" assuming that address is in active
position. We cannot change from "'" to "^", though, since doing so we
would assume that not only the interpreter, but all the methods of
processing do not distinguish between equivalent (to interpreter)
fragments, which is not true.

The use of functions in code fragments without preceding commas ","
underlines that the actual number of compiled tokens is not important.

Strictly speaking, the Act: property is a property not of a code
fragment but of its context. It is convenient to assign it to an object
in the context, though.

Special means.

We will consider each formula as surrounded by special symbols "<<" and
">>", if they do not appear in it. By default, these symbols may be
substituted by any code fragment. Hence  x == y  is a concise notation
for %A << %A >>  << x >>  ==  << y >> (which conforms with the axiom 7
given below).
Example:
      [r x '] == 'r[ >> ] x
means
      << [r x '] >>  ==  << 'r[ >> ] x

For repeating fragments we will use the following notation:
( repeat_specification ){ repeating_fragment }
For example, we will write
(5){ N }          instead of  N N N N N
(i=1..5){ N[i] }  instead of  N[1] N[2] N[3] N[4] N[5]
and so on.

Along with this notation in some cases we will use the more customary
one (namely, in cases where it is shorter), for example:
N1 .. Nm   is the same as   (i=1..m){ Ni } .

Note. The BacFORTH system [Gas94] includes the contol structures
START...EMERGE and BACK...TRACKING:
 x START y EMERGE z   ==  x  [r  y  ; ']  z
 x BACK y TRACKING z  ==  x  'r[  y  ; ]  z


            * * *

We now proceed to the formal presentation of the theory of threaded
code fragments equivalence.

Comments [not necessarily strict] in English are given in parenteses,
that facilitate understanding but not always may serve instead of
formal text and are not a part of the theory.


2.2. Axioms

(1)            '[ t >> ] >R ;    ==   t
      (placing a TCF address onto return stack and transferring control
      to it via EXIT is equivalent to execution of this TCF)

(2)            [r t '] u      ==   'r[ u ] t
      (there are two notations for placing a TCF address onto return
      stack)

(3)       If x is defined as
ÿ              : x t ;
          then
ÿ                        x    ==   [r t ; ^]

(4)        ^r[ w ] RUSH> ,f    ==   'r[ ,f w ] ;
      ( RUSH> <word> is equivalent to exit to a threaded code fragment
      that starts with <word> and continues like that which address is
      on the return stack top; see also the section 2.5)

(5)            'r[ t ] r>     ==   '[ t ]
      (the word R> moves a TCF from return stack to data stack)

(6)       ( %A N : N x == N y ) ==>  x == y
      (if for all integer N, N x is equivalent to N y, then x and y are
      equivalent)

(7)       x == y    <=>  ( %A u,v :  u x v == u y v )
      (x is equivalent to y, if and only if they have the same behaviour
      in any context (in active position); this is the definition of
      equivalence)

(8)            ^[ Act: x ]    ==  '[ x ]
      (the tick "'" means an active position)

(9)            pre[ u ] x     =>=  x
      (if a TCF is in active position, the interpreter does not process
      the addresses before it (the interpreter always "goes forwards");
      we can substitute pre[ u ] x for x, but we lose some information
      about the exact contents of memory)

(10')     ^[ ,'[ u ] v ] REF@  ==   '[ u ]

(10^)     ^[ ,^[ u ] v ] REF@  ==   ^[ u ]
      (the word REF@ receives the address of reference to a TCF, and leaves
      the address of that TCF)

(11)       ^[ ,[ u ] v ] REF+  ==   ^[ pre,[ u ]  v ]
      (the word REF@ receives the address of a TCF that starts with a
      reference (to another TCF), and leaves the address of code that
      follows the reference)

(12)   %A t   [ ; t ]  ==  ;
      (an EXIT makes the interpreter ignore the code that follows the
      EXIT)

(13)       Application of data processing operations to addresses in
           active position is a contradiction.

          Examples:
          '[ u ] REF@ --- contradiction
          '[ u ] REF+ --- contradiction

(14)  %A t == u ;  :  %E v,w :  t  ==  u ;  ==  v 'r[ w ] ;
      (an EXIT assumes an address in active position on the return stack
      top; even if the program has a bug, we may think of the return
      stack top as an address of code that hangs the system up; we will
      not examine possible equivalence of different hangups).

Notes:

1. From  u == v  it does not follow that  ^[ u ] == ^[ v ] , although
   it follows that  '[ u ] == '[ v ] .

2. We ignore possible stack underflow, i.e. [ >R R> ] == NOOP . We
   always can take a value off the stack (althought we probably cannot
   predict it in case of underflow).

3. The axiom (4) also states that
        %A u,v :   RUSH> ,f u  ==  RUSH> ,f v
   (the code that follows f is ignored by the interpreter)

4. EXIT assumes a TCF address on the return stack top, its position is
   either active or blended.

5. Later we will need some more axioms.


2.3. Definitions I


Def.1. S1( t )  is a TCF (threaded code fragment) such that
   %A N : (  N S1( t )  ==  t N  )
   ( S1( t ) behaves like t , but ignores the value on the data stack
   top)

   Examples:
      S1( DROP ) == NIP
      (Indeed, %A N   N NIP == DROP N )
      S1( SWAP ) == >R SWAP R>

Def.2. S[m]( t )  is a TCF such that
   %A N1,...,Nm :
   (  N1 ... Nm S[m]( t )  ==  t N1 ... Nm  )

   We will omit brackets when concrete numbers substitute for m, i.e. we
   will write S3 instead of S[3] .
   ( S[m]( t ) behaves like t but ignores m top stack elements)

Def.3. We will write t:S[m] , if  %E y :  t == S[m]( y ) .

Note. We will use the signature t:S[m] in the same way as adverbs and
   adjectives are used in natural languages, e.g.:
   %A N,M :  N t:S1 DROP  ==  M t DROP
   ( t:S[m] -- TCF t that ignores m top stack elements)

Def.4. We will write t:S , if  t == S1( t ) .
   ( t:S ignores stack depth and contents)

Def.5. S[-1]( t ) is a TCF such that
   S1( S[-1]( t ) ) == t
   (the "inverse operation to S1( )" )

Note. S[-1]( t ) exists not for all t .

Def.6. S[-m]( t ) is a TCF such that
   S[m]( S[-m]( t ) ) == t

   If t:S[m] , i.e. %E y :  t == S[m]( y ) , then  y == S[-m]( t ) .

In a similar maner we introduce the notions of R1, R[m], R[-m], t:R[m],
t:R.

Def.7. R1( t ) is a TCF such that
   %A N : (  N >R R1( t )  ==  t N >R  )
   ( R1( t ) behaves like t , but ignores the value on the return stack
   top)

Def.8. R[m]( t ) is a TCF such that
   %A N[1], ... N[m] :
   (i=1..m){ N[i] >R } R[m]( t )  ==  t (i=1..m){ N[i] >R }

Def.9. We will write t:R[m] , if %E y :  t == R[m]( y ) .

Def.10. We will write t:R , if  t == R1( t ) .
   (t ignores the return stack; this property is very important for us)

Def.11. R[-1]( t ) is a TCF such that
   R1( R[-1]( t ) ) == t
   (the "reversal operation" to R1( ) )

Def.12. R[-m]( t ) is a TCF such that
   R[m]( R[-m]( t ) ) == t

   Examples.
      S1( DROP )  ==  >R DROP R>  ==  NIP
      S[-1]( NIP )  ==  DROP
      S1( EXIT )  ==  DROP EXIT
      [ SWAP ]:R
      [ R> DROP ]:S
      [ ABORT ]:R:S

2.4. Simple Consequences

   This section shows how the formalism works and deduces some trivial
   but useful consequences, as evident from the common sense point of
   view as the axioms.

Statement 1.  ENTER t   ==   'r[ t >> ] >R ;
   Proof.
      In consequence of the definition   : ENTER >R ;
      ENTER t  ==  [r >R ; '] t  ==  'r[ t >> ] >R ;

Consequence. u ENTER v ;  ==  u BACK v TRACKING >R ;

Statement 2.  '[ t ] ENTER  ==  [r t ']
   Proof.
      '[ t ] ENTER  ==  '[ t ] [r >R ; ']  ==  '[ t ]  'r[ >> ] >R ;  ==
      == 'r[ >> ]  '[ t ] >R ;  ==  'r[ >> ] t  ==  [r t ']

We omit remaining proofs in this section.

Statement 3.  'r[ t ] == '[ t ] >R
Statement 4.  'r[ t ] ;  ==  t
Statement 5   'r[ t ] R1( x ) ;  ==  x t
   Proof.     'r[ t ] R1( x ) ;  ==  x 'r[ t ] ;  ==  x t
Consequence. 'r[ t ] x:R ;  ==  x t
   Proof follows from that for x:R  R1( x ) == x .
Statement 6   '[ t ] S1( u ) >R ;  == u t
Consequence. '[ t ] u:S >R ; == u t

2.5. Practically Important Statements

Statement 1. (The theorem of 1-st order call equivalence)

ÿ  [r R1( t ) ; ']  ==  t

   Proof.
      [r R1( t ) ; ']  ==  'r[ >> ] R1( t ) ;  ==
      ==  t 'r[ >> ] ;  ==  t >>  ==  t

   (A call of R1( t ) is equivalent to t . You will recall that R1( t )
   behaves like t but ignores the return stack top)

Consequence. (Possibility of inline substitution for t:R)
ÿ  t:R  ==  [r t ; ']

Note. This statement reflects the essence of problems that appear with
   inlining)

Example:
   R>  == [r R1 ( R> )  ; '] == [r R> R> SWAP >R ; '] , therefore one
   can redefine R> like following:
   : R> ( -- a ) ( R: a -- ) R> R> SWAP >R ;

Statement 2.  PRO  ==  R> >L  'r[ LDROP ; ]
   Proof.
      Because of the definition
      : PRO R> R> >L ENTER LDROP ;

      PRO  ==  [r R> R> >L ENTER LDROP ; ']  ==
      ==  'r[ >> ]  R> R> >L  'r[ LDROP ; ] >R ;  ==
      ==   '[ >> ]     R> >L  'r[ LDROP ; ] >R ;  ==
      ( because [ R> >L 'r[ LDROP ; ] ]:S )
      ==  R> >L 'r[ LDROP ; ] '[ >> ] >R ;  ==
      ==  R> >L 'r[ LDROP ; ]

      (PRO is a BacFORTH [Gas94] word that complements 1-st order call
      (i.e. ordinary one) to 2-nd order call (that is used for
      backtrackable code))

Statement 3   f  ==  [r u ']   ==>   [r v:R1 RUSH> ,f ']  ==  [r v u ']

      (if f is a colon definition

      : f u ;   \ formulation of the statement implies that  u ; == u

      and v ignores at least the top of return stack, then

      : x v RUSH> f ;

      is equivalent to

      : x v u ; )

   Proof.
      [r v:R1 RUSH> f ']  ==
      ==  [r v ; '] f  ==
      ==  [r v ; '] [r u ']  ==
      ==  R[-1]( v ) 'r[  'r[ >> ]  u ] ;  ==
      ==  R[-1]( v )  'r[ >> ]  u  ==
      ==  'r[ >> ]  v  u  ==
      ==  [r  v u  ']

Consequence.  'r[ w ] RUSH> ,f  ==  'r[ w ] u
   Proof.
      'r[ w ] RUSH> f  ==  [r RUSH> f '] w  ==  [r u '] w

      (the use of RUSH> f is equivalent to substituting the definition
      of f inline, including the EXIT that follows it)

Note. The word RUSH> (either of [Gas93, Gas93R, Gas94]) is called GOTO
in F-PC. It allows to get rid of a superfluous value at the return
stack, which is important in BacFORTH.

We would like to proceed to construction and description of 2nd order
threaded code. But what we have already presented is not enough to
define it, neither for confident code fragments analysis. Therefore
the next our goal will be a study of code fragments properties.


2.6. The Properties S[m] and R[m]

It goes without saying that the statements given below are valid only
if the fragments S[m]( t ) and R[m]( t ) exist. The question about
existance of S1( t ) for any t remains to be investigated. There is
reason to think that it exists for any t.

Statement 1.  S1( S1( t ) )  ==  S2( t )
   Proof.
      %A N : %A M :
      N M S1( S1( t ) )  ==  N S1( t ) M  ==  t N M

Statement 2.  t  ==  S1( t )   =>   %A m : t:S[m]
   Proof.
      %A m
      t  ==  S1( t )  ==  S1( S1( t ) )  ==  ...  ==  S[m]( t )
      => %A m %E y == t : t == S[m]( y )   <=>   %A m  t:S[m]

Note. The reverse is not true.
      Consider the following definition:
      VARIABLE X
      : XX DEPTH X ! ;
      For the word XX for any m exists S[-m],
      S[-m]( XX ) ==  DEPTH m + X !
      but
      S1( XX )  ==  [ DEPTH 1 - X ! ]  =/=  XX

We omit the remaining proofs in this section.

Statement 3.  %A N :  N S1( t ) DROP  == t
Statement 4.  t:S1  <=>  %A N : (  S1( N t DROP )  ==  t  )
Consequence.  %A N : ( S[-1]( t )  ==  N t DROP )
Statement 5.  S[-1]( S1( t ) )  ==  t
Note.  By definition of S[-1]( t ),    S1( S[-1]( t ) ) == t
Statement 6.  ( The theorem of comparison by S[-1] )
      if t:S1, u:S1 then
ÿ     S[-1]( t )  ==  S[-1]( u )  <=>  t == u
Statement 7.  ( The theorem of comparison by S1 )
ÿ     S1( t )  ==  S1( u )  <=>  t == u
Statement 8   If S1( t ), S1( u ) exist, then S1( t u ) == S1( t ) S1( u )
Consequence. [t:S1 u:S1]:!S1
Statement 9   u:S1, v:S1 =>   S[-1]( u ) S[-1]( v )  ==  S[-1]( u v )
Statement 10. If t:S2, then  S[-1]( S[-1]( t )) == S[-2]( t )

Definition 1.  S[0]( t ) == t

Statement 11. For any integer n and m
ÿ     S[n]( S[m]( t ) ) == S[n+m]( t )
      if the mentioned fragments exist.
Note.
ÿ     Obviously, analogous statements may be proven for the return
ÿ     stack, with the only difference in proofs that S[m] will be
      replaced by R[m]. Therefore we will apply statements 1 - 11 to
      return stack as well, denoting them as Statement 1R - Statement 11R.

Statement 12  R1( S1( t ) )  ==  S1( R1( t ) )
Statement 13  S1( t:R ):!R

Statement 14  S1( t:R )  ==  >R t R>
   Proof.
      N S1( t:R )  ==   t N  ==  t N >R R>  ==  N >R R1( t:R ) R>  ==
      ==  N >R t R>

2.7. About BRANCH instructions

In this section we will show that presence of BRANCH instructions
(BRANCH and ?BRANCH) in threaded code still permits considering threaded
code fragments as sequences of compiled functions that are processed one
by one. (The words BRANCH and ?BRANCH are compiled by control structure
words IF , WHILE , REPEAT , etc.)

Definition 1. BRANCH    ==   [r R> REF@ >R ; ^]
   (BRANCH may be defined as : BRANCH R> REF@ >R ; )

Statement 1   BRANCH ,[ x >> ]  ==   x
   (A jump to x is equivalent to x)
   Proof.
      BRANCH ,[ x >> ]   ==
      ==   [r  R> REF@ >R ;  ^]  ,[  x >>  ]   ==
      ==   ^r[ ,[  x >>  ] ]  R> REF@ >R ;   ==
      ==   ^[ ,[  x >>  ] ]  REF@ >R ;   ==
      ==   ^[  x >>  ]   >R ;   ==   x >>   ==   x

Axiom B1. ?BRANCH ,[ !Act: u ] !Act: v
   i.e. in
   [ ?BRANCH ,[ u ] v ]
   both u and v are in active position.

Definition 2. N?BRANCH ,[ u ]   ==   0= ?BRANCH ,[ u ]
      ( ?BRANCH - jump to u if false; N?BRANCH - jump to u if true)

Axiom B2. ?BRANCH ,[ u ]    ==   N?BRANCH ,[ >> ] u
      (Any one may be used for control flow splitting)

Axiom B3. S1( x ) ?BRANCH ,[ u ] v  ==  ?BRANCH ,[ x u ] x v
      (A TCF of which the branch condition does not depend, may be moved
      inside the IF statement)

Axiom B4. DUP ?BRANCH ,[ u ] S1( x ) ?BRANCH ,[ v ] y  ==
ÿ     DUP ?BRANCH ,[ u ] DROP x y
      (no need in double checking of the same condition)

Statement 2.  %A N :   N SWAP ?BRANCH ,[ u ] v  ==  ?BRANCH ,[ N u ] N v
      (factoring a literal out of IF statement)
   Proof.
      S1( N ) ?BRANCH ,[ u ] v  ==  ?BRANCH ,[ N u ] N v

Definition 3. if( u | v )    ==   ?BRANCH ,[ v >> ]  u BRANCH ,[ >> ]
      (the structure IF u ELSE v THEN compiles code like this)

Statement 3   By Statement 1 and definition of if( | )
ÿ     if( u | v )    ==   ?BRANCH ,[ v >> ]  u >>

      Note that the continuation >> is common for both branches of the
      if statement. It should be noted we obtained this important
      feature as a feature of notation.

Statement 4   if( u | v ) w  ==  if( u w | v w )
   Proof.
      By Statement 2
      if( u | v ) w  ==  ?BRANCH ,[ v w >> ] u w >>  ==  if( u w | v w )

Statement 5   S1( x )  if( u | v )   ==   if( x u | x v )
   Proof. Follows from the properties of ?BRANCH .

Statement 6   ?BRANCH  ==  [r if( R> REF+ >R | R> REF@ >R ) ; ^]
      (?BRANCH may be correctly redefined as
      : ?BRANCH IF R> REF+ >R ELSE R> REF@ >R THEN ;
      i.e. the new definition will be equivalent to the old one)
   Proof.
      [r  if(  R> REF+ >R  |  R> REF@ >R  )  ; ^]  ,[ u ]   ==
      ==   ^r[ ,[ u ]  >>  ]:S  if(  R> REF+ >R  |  R> REF@ >R  )  ;   ==
      ==   if(  ^r[  ,[ u ]  >>  ]   R> REF+ >R ;
             |  ^r[  ,[ u ]  >>  ]   R> REF@ >R ;  )   ==
      ==   if(  ^[ pre ,[ u ]  >> ]  >R  ;
             |             ^[  u  ]  >R  ;  )   =>=
      ==   if(             '[  >> ]  >R  ;
             |             '[  u  ]  >R  ;  )   =>=
      =>=  if( >> | u )  ==  ?BRANCH ,[ u ]

      (The symbol =>= shows that we lose information about the location of
      threaded code fragments)

We omit the proofs of two following statements.
Statement 7   S1( if( u | v ) )  ==  SWAP if( S1( u ) | S1( v ) )
Statement 8   DUP S1( if( u | v ) w ) if( y | z )  ==
      if( u w y | v w z )

So, a program may be represented as a tree, probably infinite, in
which any path from root to one of the leaves may correspond to a set
of input data values.

Since these paths cover all the possible behaviours of the program,
we may prove statements that are true for any particular path, i.e.
we work with a fragment of [ u ?BRANCH ,[ v ] w ] type as with two
"linear" fragments  [ u DROP v ]  and  [ u DROP w ].

Thus, we can consider code fragments with branches as "usual",
"linear" threaded code fragments, knowing that presence or absence of
branches does not affect any features of interest.

Note.
   Note that for a fragment with a loop, e.g.
   z  ==  BEGIN t1 x t2 AGAIN
   exists a representation in the form of
   z  ==  v x w
   where  v  ==  t1  and  w  ==  t2 z

Note.
   For the following fragment:
   z  ==  u1 [r t1 x t2 '] u2
   such a representation also exists:
   z  ==  v x w
   where   v  ==  u1 'r[ u2 ] t1   and   w  ==  t2

Note.
   As mentioned above, we consider a loop statement as a concise
   notation for an infinite code fragment (or its equivalent). Taking
   into account that our goal is a study of control transfer and return
   addresses manipulations, this representation is wholly satisfactory.

3. DISCUSSION

The calculus presented enables one to analyse control flow changes
without going into details. This aids its use by a human and makes its
use on computers more difficult.

The two notations for a call - [r x '] y and 'r[ y ] x - reflect its
dual nature: on the one hand, it x gets enclosed into a context; on the
other hand it is just placng the address of continuation onto the return
stack. Depending on whether we focus upon x or [r ... '] y (its
context), we will use one or the other notation, which one will be more
convenient.

The calculus is based on the notion of equivalence and does not use the
notion of stack. Furthermore, we do not distinguish code that
necessarily executes from code that may never execute: both are
particular cases of active position. This enables us to avoid special
analysis of cases where e.g. exception mechanism comes into action.

From intuitive viewpoint, two code fragments are equivalent if they have
the same sense. The notion of equivalence allowed us to use, in effect,
the intuitively understood notion of sense without mentioning it.

The concept of virtual theorist enabled us to perform a study of
threaded code equivalence with only intuitive understanding of this
notion and formulate a definition later. The use of common sense enabled
us to avoid too early formulation of definitions. It turned out that
mistakes happen mostly in the definitions; the theorems are just their
consequences. A theory cannot be created in the same order that it gets
presented. Axiomatic approach enables us to drive fastly, but fast
driving requires at least a known road. In a new area, much work has to
be done before we can formulate axioms, and only common sense (that is,
unformalized expert knowledge) can help there, since the axioms and
definitions can be considered only as hypotheses. The knowledge
modularity allowed us later replace intuitive notions by strict
definitions.

4. RESULTS

The concept of position (active, passive, etc.) is introduced that
represents the differences between code, data, self-modifying code, etc.

A notation is developed that adequately describes processing of
[threaded] code by the code interpreter and effect of return address
manipulations on it. Formal description of how return addresses
manipulations are reflected in the control flow changes is given. The
calculus enables one to analyse return addresses manipulations, prove
their correctness, perform equivalent transformations of code fragments.

The theorem of 1-st order call equivalence is proved, that clarifies the
cases where inline substitution cannot be used instead of a call, which
is the key to construction of optimizing compilers for forth.

The approach to theory construction introduces modularity of theoretical
knowledge.

6. ACKNOWLEDGEMENTS

The author thanks S.N.Baranoff and V.A.Tuzov for discussions and notes
about this material.

7. REFERENCES

[BaN88R] Baranoff S.N., Nozdrunoff N.R. Jazyk Fort i ego
         realizatsii. - L:Mashinostroenie, 1988. (The Forth
         Language and Its Implementations, in Russian.)

[Cha91] Charlton, Gordon. "FOSM, A FOrth String Matcher".
         Proc. of the EuroFORML'91 Conf., 1991.

[Gas93]  Gassanenko M.L. Multi-FCA DOES>: Implementation via
         Self-Modifying Code. Proc. of the euroFORTH'93 conference,
         held from October 15th-18th 1993 at the museum of Marianske
         Lazne (Marienbad), Czech Republic, 8 p.

[Gas93R] Gassanenko M.L.
         Novye sintaksicheskie konstruktsii i be`ktreking dlja jazyka
         Fort.//Problemy tehnologii programmirovanija - SPb: SPIIRAN,
         1991-93, p.148-162. (New Control Structures and Backtracking
         for the Forth Language, in Russian.)

[Gas94]  Gassanenko, M.L. BacFORTH: An Approach to New Control
         Structures. Proc. of the EuroForth'94 conference, 4-6 November
         1994, Royal Hotel, Winchester, UK, p.39-41.

[Poi91]  Poial J. Multiple Stack-effects of Forth Programs. 1991 FORML
         Conference Proceedings, euroFORML'91 Conference, Oct 11-13,
         1991, Marianske Lazne, Czechoslovakia, Forth Interest
         Group, Inc., Oakland, USA, 1992, 400-406.

[Poi93]  Poial J. Some Ideas on Formal Specification of Forth Programs.
         9th euroFORTH conference on the FORTH programming language and
         FORTH processors, Oct 15-18, 1993, Marianske Lazne, Czech
         Republic, 1993, 4 pp.

[Poi94]  Poial, Jaanus. Forth and Formal Language Theory. Proc. of the
         EuroForth'94 conference, 4-6 November 1994, Royal Hotel,
         Winchester, UK, 6 pp.

[Rod90a] Rodriguez, B. A BNF Parser in Forth. ACM SIGForth
         Newsletter, vol.2, no.2, December 1990, p.13-18.

[Rod90b] Rodriguez, Bradford J. Rules Evaluation Through
         Program Execution. Proc. of the 1990 Rochester Forth
         Conf., p.123-125.

[StK92]  Stoddart B., Knaggs P. The (Almost) Complete Theory of Forth
         Type Inference. Proc. EuroForth Conference 1992.

[StK93]  Stoddart B., Knaggs P. Type Inference in Stack Based Languages.
         Formal Aspects of Computing, BCS, 1993, 5, 289-298.

[Sto93]  Stoddart B. Self Reference and Type Inference in Forth. 9th
         euroFORTH conference on the FORTH programming language and
         FORTH processors, Oct 15-18, 1993, Marianske Lazne, Czech
         Republic, 1993, 9 pp.

[Tuz88R] Tuzov V.A.
         Funktsional'nye metody programmirovanija./ Instrumentalnye
         sredstva programmirovanija - L:LIIAN, 1988. - p.129-143. (The
         Functional Methods of Programmming, in Russian)

[Tuz90R] Tuzov V.A.
         Jazyki predstavlenija znanij. - L:LGU, 1990. (The Languages of
         Knowledge Representation [what an ideal language of knowledge
         representation should be], in Russian.)