tests/rewriting7.pcc

   1 ///////////////////////////////////////////////////////////////////////////////
   2 //
   3 //  This example program performs simplification of first order logic
   4 //  formulas using rewriting.  We'll use topdown rules for this.
   5 //
   6 ///////////////////////////////////////////////////////////////////////////////
   7 #include <iostream.h>
   8 #include <AD/strings/quark.h>
   9 #include <AD/generic/generic.h>
  10
  11 datatype Wff = T                  => "true"
  12              | F                  => "false"
  13              | Var Id             => _
  14              | And Wff, Wff       => '(' _ "and" _ ')'
  15              | Or  Wff, Wff       => '(' _ "or" _ ')'
  16              | Not Wff            => "not" '(' _ ')'
  17              | Implies Wff, Wff   => '(' _ "=>" _ ')'
  18              | Predicate Id, Ids  => _ _
  19              | Exists Id, Wff     => "exists" _ '.' _
  20              | Forall Id, Wff     => "forall" _ '.' _
  21 and Ids :: printable = #() | #( Id ... Ids )
  22 where type Id = class Quark
  23 ;
  24
  25 ///////////////////////////////////////////////////////////////////////////////
  26 //
  27 //  Function to check that an identifier occurs free in a wff.
  28 //
  29 ///////////////////////////////////////////////////////////////////////////////
  30 Bool is_free (Id id, Wff wff)
  31 {  match (wff)
  32    {  T || F:         { return true; }
  33    |  Var x:          { return id != x; }
  34    |  And(a,b):       { return is_free(id,a) && is_free(id,b); }
  35    |  Or(a,b):        { return is_free(id,a) && is_free(id,b); }
  36    |  Implies(a,b):   { return is_free(id,a) && is_free(id,b); }
  37    |  Not a:          { return is_free(id,a); }
  38    |  Exists(a,b):    { return a == id || is_free(id,b); }
  39    |  Forall(a,b):    { return a == id || is_free(id,b); }
  40    |  Predicate(_,l): { Ids ids = l;
  41                         match while (ids)
  42                         {  #():                  { return true; }
  43                         |  #(x ... _) | x == id: { return false; }
  44                         |  #(_ ... t):           { ids = t; }
  45                         }
  46                       }
  47    }
  48 }
  49
  50 instantiate datatype Wff, Ids;
  51
  52 void transform(Wff wff)
  53 {
  54    cout << "Input: " << wff << endl;
  55
  56    rewrite (wff) type (Wff)
  57    {
  58    topdown:
  59
  60       // Transform into prenex normal form
  61
  62       Forall(x,Not(P)):  Not(Exists(x,P))
  63    |  Exists(x,Not(P)):  Not(Forall(x,P))
  64    |  Forall(x,And(P,Q)): And(Forall(x,P),Forall(x,Q))
  65    |  Exists(x,Or(P,Q)):  Or(Exists(x,P),Exists(x,Q))
  66    |  Exists(x,And(P,Q)) | is_free(x,Q): And(Exists(x,P),Q)
  67    |  Exists(x,And(P,Q)) | is_free(x,P): And(P,Exists(x,Q))
  68    |  Forall(x,Or(P,Q))  | is_free(x,Q): Or(Forall(x,P),Q)
  69    |  Forall(x,Or(P,Q))  | is_free(x,P): Or(P,Forall(x,Q))
  70    |  Forall(x,P) | is_free(x,P): P
  71    |  Exists(x,P) | is_free(x,P): P
  72
  73    |  Or(T, _):    T
  74    |  Or(_, T):    T
  75    |  Or(F,X):     X
  76    |  Or(X,F):     X
  77    |  And(F,_):    F
  78    |  And(_,F):    F
  79    |  And(T,X):    X
  80    |  And(X,T):    X
  81    |  Not(T):      F
  82    |  Not(F):      T
  83    |  Not(Not(X)): X
  84    |  Implies(X,Y): Or(Not(X),Y)
  85    }
  86
  87    cout << "Output: " << wff << endl;
  88 }
  89
  90
  91 int main()
  92 {
  93    Wff wff;
  94
  95    wff = Implies(Exists(#"w",Forall(#"x",Predicate(#"P",#(#"w",#"x")))),
  96                  Forall(#"y",Exists(#"z",Predicate(#"P",#(#"z",#"y")))));
  97    transform(wff);
  98
  99    wff = Forall(#"w",Forall(#"y",Exists(#"x",Exists(#"z",
 100               Implies(Predicate(#"P",#(#"w",#"x")),
 101                       Predicate(#"P",#(#"z",#"y")))))));
 102    transform(wff);
 103    wff = Forall(#"w",Forall(#"y",Exists(#"x",
 104              Implies(Predicate(#"P",#(#"w",#"x")),
 105                      Predicate(#"P",#(#"x",#"y"))))));
 106    transform(wff);
 107
 108    return 0;
 109 }