previous up next Previous: 4.2 More than Complete
Up: 4. Completeness
 Next: 5. Conclusions


   
4.3 Turing Completeness

This section addresses the Turing completeness of OCL. It is relatively easy to show that the language is not complete, moreover, that the functions expressible in OCL are all primitive recursive. In order to prove so, we show that LOOP-programs can and WHILE-programs cannot be written in OCL (see [Sch95]).

The syntax of LOOP-programs is as follows:


    P  ::= X - X + C
       | X -  X - C
       | LOOP X DO P END
       | P ; P
    X  ::= x0 | x1 | x2 | ... (variables)
    C  ::=0|1|2| ... (constants)

The semantics of LOOP-programs is straightforward. Given a LOOP-program that computes a k-ary function f, it is assumed that the input values n_1,\ldots,n_k are initially stored in the variables x_1,\ldots,x_k, that any other variable has initial value 0, and that the result f(n_1,\ldots,n_k) is stored in the variable x0 after execution of the program. The value assignment xi <- xj + c is interpreted as usual, that is, the new value of the variable xi is the value of xj plus c. The value assignment xi <- xj - c is the non-negative subtraction, that is, if c > xj then the new value of xi is 0 otherwise the value of xj minus c. A LOOP-program of the form P1 ; P2 is interpreted as the execution of P1 and afterwards the execution of P2. Finally a LOOP-program of the form LOOP xi DO P END is interpreted as follows: the program P is executed ntimes, where n is the value of the variable xi at the beginning (i.e. the change of the value of xi within P does not affect the number of repetitions).

LOOP-programs are WHILE-programs, and additionally if P is a WHILE-program then


\texttt{WHILE } x_i \neq 0 \texttt{ DO } P \texttt{ END}
is a WHILE-program. The semantics of the new construct is the following: the program P is repeatedly executed as long as the value of xi is different from 0.
(Obviously the LOOP construct becomes superfluous, LOOP
x DO P ENDcan be simulated by \texttt{WHILE } y \neq 0 \texttt{ DO }
y := y-1 \texttt{ ; }P \texttt{ END}.)

Every LOOP-program can be computed by an OCL expression. Indeed, given a LOOP-program P computing a k-ary function and using auxiliary variables x_{k+1},\ldots,x_r, we write an OCL expression that manipulates an array vals1 of r+1values (representing the values of the variables x_0,\ldots,x_r) and returns the first value of this array after executing the translation of P:

\begin{array}{l}
\verb* ...

The return value of the above expression is the first value of the sequence vals1 after iterating one time the execution of \ensuremath{\textit{trans}} (P,1). Initially vals1 stores the value ni for the variable xi ( i=1,\ldots,k) and 0 otherwise. The return value of \ensuremath{\textit{trans}} (P,1) is stored in vals1. The function \ensuremath{\textit{trans}} (P,n) with n \in \ensuremath{\mathsf{I\kern-.1em N}} is a function that manipulates the sequence valsn and is defined by induction on the structure of P as follows:

The natural number n accompanying the definition of \ensuremath{\textit{trans}} allows for the definition of new variables that do not shadow previously (in the outer block) defined ones.

So for instance the function f(n,m)=n+m, computed by the program

    X0 <- X1 + X2
which can be encoded as the following LOOP-program P
    X0 <- X1 + 0 ;    -- P1
    LOOP X2 DO        -- P2
        X0 <- X0 + 1  -- P21
    END
is translated to the OCL expression obtained by successively calculating \ensuremath{\textit{trans}} as follows:

1.
Sequence{1..1}->iterate(
i : Integer ;
vals1 : Sequence(Integer) = {0,n,m}
|   trans(P,1)
)->first

2.
Sequence{1..1}->iterate(
i : Integer ;
vals1 : Sequence(Integer) = {0,n,m}
|   Sequence{1..2}->iterate(
    step : Integer ;
    vals2 : Sequence(Integer) = vals1
    |   if step = 1
        then trans(P1,2)
        else trans(P2,2)
        endif
)   )->first

3.
Sequence{1..1}->iterate(
i : Integer ;
vals1 : Sequence(Integer) = {0,n,m}
|   Sequence{1..2}->iterate(
    step : Integer ;
    vals2 : Sequence(Integer) = vals1
    |   if step = 1
        then vals2->iterate(
             val : Integer ;
             newvals : Sequence(Integer) = Sequence{}
             |   if newvals->size = 1
                 then (newvals->subSequence(1,0))
                      ->append(val+0)
                      ->union(newvals->subSequence(0+2,1))
                      ->append(val)
                 else newvals->append(val)
                 endif
             )
        else Sequence{1..vals2->at(2+1)}->iterate(
             i : Integer ;
             vals3 : Sequence(Integer) = vals2
             |   trans(P21,3)
             )
        endif
)   )->first

4.
Sequence{1..1}->iterate(
i : Integer ;
vals1 : Sequence(Integer) = {0,n,m}
|   Sequence{1..2}->iterate(
    step : Integer ;
    vals2 : Sequence(Integer) = vals1
    |   if step = 1
        then vals2->iterate(
             val : Integer ;
             newvals : Sequence(Integer) = Sequence{}
             |   if newvals->size = 1
                 then (newvals->subSequence(1,0))
                      ->append(val+0)
                      ->union(newvals->subSequence(0+2,1))
                      ->append(val)
                 else newvals->append(val)
                 endif
             )
        else Sequence{1..vals2->at(2+1)}->iterate(
             i : Integer ;
             vals3 : Sequence(Integer) = vals2
             |   vals3->iterate(
                 val : Integer ;
                 newvals : Sequence(Integer) = Sequence{}
                 |   if newvals->size = 0
                     then newvals->append(val+1)
                     else newvals->append(val)
                     endif
             )   )
        endif
)   )->first

We now prove that the OCL expression defined in terms of a LOOP-program computes the same function.

Proposition 1   Let P be a LOOP-program used in a context where only variables among x_1,\ldots,x_r are used. For any natural numbers m_1,\ldots,m_r,m'_1,\ldots,m'_r \in \ensuremath{\mathsf{I\kern-.1em N}} , for any natural number n \in \ensuremath{\mathsf{I\kern-.1em N}} , if the variable xi changes its value from mi to m'i ( i=1,...r ) after the execution of P, then valsn changes its value from {m0,...,mr } {m'0,...,m'r } after the execution of \ensuremath{\textit{trans}} (P,n).

Proof 1   The thesis is proved by induction on the structure of P.

Hence, every LOOP-computable function is also computable using an OCL expression.

Consider now the WHILE construct of WHILE-programs. The iterating construct iterate runs through a collection (randomly ordered if not a sequence) from its beginning to its end. Thus, an iterate terminates if, and only if, the collection is finite. Notice that, on the one hand and according to [RAT97, p. 13], there are three ways of getting a collection:

1.
by a literal, e.g. Set{1,2,5,3}, or
2.
by a navigation, e.g. Polygon self.vertices, or
3.
by operations on collections, e.g. set->union(set2).
The first two possibilities return a finite collection, and finite collections are closed under the operations mentioned as third possibility.5 But, on the other hand, the feature allInstances associated with the type oclType of types returns a set; see [RAT97, p. 20]. That is, by writing Integer.allInstances (or even Real.allInstances) we could also obtain an infinite collection.

In any way, an iterate either performs a previously determined number of iterations or does not terminate, since there is no possibility of interrupting an iterate (like e.g. the break command of C). In other words, the WHILE construct cannot be encoded in OCL, and thus semidecidable problems in general cannot be solved in OCL.

Therefore, given that the class of primitive recursive functions coincides with the class of LOOP-computable functions and that the class of \mu-recursive functions coincides with the class of WHILE-computable functions (see [Sch95]), OCL allows only for the definition of primitive recursive functions (or totally undefined functions if Integer.allInstances is a valid OCL expression).