Courses/CS 460/Fall 2005/Concurrent logic programming in Oz/Example

From CSWiki

Here is the Oz code for the ubiquitous append/3. It is being run with {Append Xs Ys [a b]}, which asks for Xs and Ys, which when appended will result in the list [a b].

local
   proc {Append Xs Ys Zs}
      choice
	 Xs = nil 
         Ys = Zs
      [] X Xr in
	 Xs = X | Xr
	 Zs = X | {Append Xr Ys}
      end
   end
in
   {Browse {SearchAll
	    proc {$ Ans} Xs Ys in
	       Ans = Xs#Ys
	       {Append Xs Ys [a b]} end}}
end

Here are the sequences of steps this program takes along with the sets of statements that are true after each step. In the following we leave out the unification statements and simply make the relevant substitutions. Also, we don't show variables that do not yet have values. We show in bold the final statement sets.

We start with the set {Zs = [a b]; Ans = Xs#Ys}. We immediately reach a choice statement.

1. In the first branch of the choice: {Xs = nil; Ys = Zs = [a b]; Ans = nil#[a b]}. This terminates the computation along this path
2. In the second branch of the choice, we continue as follows.
   {Xs = a | Xr; Zs = [a b]; Ans = (a | Xr)#Ys}. We then make the call {Append Xr Ys [b]}. Again there are two choices.
   1. In the first branch, we have the following.
      {Xr = nil; Xs = [a] = a | Xr; Ys = [b]; Zs = [a b]; Ans = ([a]#[b]}.
      This ends the computation along this path.
   2. In the second branch, we continue as follows. Our set of true statements becomes:
      {Xr = b | Xr'; Xs = a | Xr; Zs = [a b]; Ans = (a | b | Xr')#Ys}.
      Once again we make a recursive call: {Append Xr' Ys nil}. Again there are two choices.
      1. In the first:
         {Xr' = nil; Xr = b | Xr' = [b]; Xs = a | Xr = [a b]; Ys = nil; Zs = [a b]; Ans = [a b]#nil}.
         This ends the computation along this path.
      2. In the second choice branch, we get:
         {Xr' = X | Xr''; Xr = b | Xr'; Xs = a | Xr; Zs = [a b]; Ans = [a b]#Ys}.
         But the second unifcation in this branch fails because nil cannot unify with X | _. So this computation fails.

   This ends all computations. We have three results. Expressed as conjunctions and with all the variables showing, they read as follows.

   1. Xs = nil & Ys = Zs = [a b] & Ans = Xs#Ys = nil#[a b]
   2. Xr = nil & Xs = a | Xr = [a] & Ys = [b] & Zs = [a b] & Ans = Xs#Ys = ([a]#[b]
   3. Xr' = nil & Xr = b | Xr' = [b] & Xs = a | Xr = [a b] & Ys = nil & Zs = [a b] & Ans = Xs#Ys = [a b]#nil