Examples

We want to clarify the ideas of our analysis by providing some simple examples. If the type environment E contains only one type annotation $TA$ for the function in the left-hand side of the rule $r$, we simply write instead of .

 

Now we want to study some more interesting examples where nondeterminism occurs.

 

We want to provide a final example to show the APP rule for a function call.

 

The first step in the analysis will always be the typing of a given program. In the second step, an expression to be evaluated w.r.t. to the program is analysed. For instance, if we would like to evaluate  $$f 1  w.r.t. the program from Example 5, the analysis returns

signalizing that this expression will reduce deterministically. In contrast, for  $$f x  the result is

Thus, the computation will split while evaluating  $$f x.