fun comparison between solving static Twelf indexed type family relations & dynamic Oz relational computation functions

Solve.oz

% $Id: Solve.oz,v 1.1 2007/11/26 20:13:05 leavens Exp leavens $
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Mozart System Supplements

% This file gives the extensions to the basic Mozart system that
% are used in the book "Concepts, Techniques, and Models of Computer
% Programming".  The contents of this file can be put in the .ozrc
% file in your home directory, which will cause it to be loaded
% automatically when Mozart starts up.

% Authors: Peter Van Roy and Seif Haridi
% May 9, 2003

declare

% ... I took out the stuff from other chapters... Gary T. Leavens

%%%%%%%%%%%%%%%%%%%%%%%%%%% Chapter 9 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Lazy problem solving (Solve)

% This is the Solve operation, which returns a lazy list of solutions
% to a relational program.  The list is ordered according to a
% depth-first traversal.  Solve is written using the computation space
% operations of the Space module.

local
   fun {SolStep S Rest}
      case {Space.ask S}
      of failed then Rest
      [] succeeded then {Space.merge S}|Rest
      [] alternatives(N) then 
         {SolLoop S 1 N Rest}
      end
   end

   fun lazy {SolLoop S I N Rest}
      if I>N then Rest
      elseif I==N then
         {Space.commit S I}
         {SolStep S Rest}
      else Right C in
         Right={SolLoop S I+1 N Rest}
         C={Space.clone S}
         {Space.commit C I}
         {SolStep C Right}
      end
   end
in
   fun {Solve Script}
      {SolStep {Space.new Script} nil}
   end
end

UnarySum.elf

nat : type.
zero : nat.
suc : nat -> nat.

sum : nat -> nat -> nat -> type.
sum/zero : sum zero N N.
sum/suc : sum (suc M) N (suc P)
   <- sum M N P.
%mode sum +M +N -P.
%worlds () (sum _ _ _).
%total M (sum M _ _).

%%% Example %%%

M = (suc (suc zero)).
N = (suc (suc (suc zero))).
P = (suc (suc (suc (suc (suc zero))))).
%solve _ : sum M N P.

%%% Output %%%

% _ : sum M N P = sum/suc (sum/suc sum/zero).

UnarySum.oz

\insert 'Solve.oz'

fun {Nat}
   choice
      zero
   []
      suc({Nat})
   end
end

fun {Sum M N P}
   choice
      M=zero
      N=P
      sum_zero#M#N#P
   []
      M2 P2 in
      M=suc(M2)
      P=suc(P2)
      sum_suc({Sum M2 N P2})#M#N#P
   end
end

%%% Example %%%

declare
M=suc(suc(zero))
N=suc(suc(suc(zero)))
P=suc(suc(suc(suc(suc(zero)))))

{Show {Solve fun {$} {Sum M N P} end}}

%%% Output %%%

% [sum_suc(
%     sum_suc(
%        sum_zero#zero#suc(suc(suc(zero)))#
%        suc(suc(suc(zero))))#
%     suc(zero)#suc(suc(suc(zero)))#suc(suc(suc(suc(zero)))))#
%  suc(suc(zero))#suc(suc(suc(zero)))#
%  suc(suc(suc(suc(suc(zero)))))]