[an error occurred while processing this directive]

{***************************************************************************}
{* SYNTAX OF A SUB-LANGUAGE OF FP                                          *}
{***************************************************************************}

type OBJECTS
  basedon NAT, BOOL
  sort Obj
  cons bobj : (Bool)Obj,
       nobj : (Nat)Obj,
       pair : (Obj,Obj)Obj
endoftype
complete OBJECTS
noetherian OBJECTS
display OBJECTS bobj = "_",
                nobj = "_",
                pair = "<_,_>"

type FORMS
  basedon ID, NAT, BOOL
  sort Form
  cons id, p_1, p_2,                                        {Id., Proj.}
       eqz, s, p, ad, su, mu : Form,                     {Basisfct. NAT}
       bconst : (Bool)Form,
       nconst : (Nat)Form,
       iconst : (Id)Form,
       comp, tuple : (Form,Form)Form,
       cond : (Form,Form,Form)Form
endoftype
complete FORMS
noetherian FORMS
display FORMS bconst = "_~",
              nconst = "_~",
              iconst = "_",
              comp = "(_ o _)",
              tuple = "[_, _]",
              cond = "if _\  then _\  else _\endif"

type DECLARATIONS
  basedon FORMS, ID, BOOL
  sort Decls
  cons emptydecls : Decls,
       declare : (Decls,Id,Form)Decls
  func body : (Decls,Id)Form
  axioms all (i,j : Id, e : Decls, f : Form)
    body(declare(e,i,f),i) -> f,
    equal_Id(i,j) = false => body(declare(e,i,f),j) -> body(e,j)
endoftype
complete DECLARATIONS except body
noetherian DECLARATIONS
display DECLARATIONS emptydecls = "",
                     declare = "_\_ <= _"

{***************************************************************************}
{* EVALUATION                                                              *}
{***************************************************************************}

type FP
  basedon DECLARATIONS, FORMS, OBJECTS, ID, NAT, BOOL
  func eval : (Decls,Form,Obj)Obj 
  axioms all (a, b : Bool, m, n : Nat, f, g, h : Form, x, y : Obj,
              e : Decls, i : Id)
    eval(e,id,x) -> x,
    eval(e,p_1,pair(x,y)) -> x, 
    eval(e,p_2,pair(x,y)) -> y, 
    eval(e,iconst(i),x) -> eval(e,body(e,i),x),
    eval(e,eqz,nobj(n)) -> bobj(equal_Nat(n,0)),
    eval(e,s,nobj(n)) -> nobj(succ(n)),
    eval(e,p,nobj(n)) -> nobj(pred(n)),
    eval(e,ad,pair(nobj(m),nobj(n))) -> nobj(add(m,n)),
    eval(e,su,pair(nobj(m),nobj(n))) -> nobj(sub(m,n)),
    eval(e,mu,pair(nobj(m),nobj(n))) -> nobj(mult(m,n)),
    eval(e,bconst(a),x) -> bobj(a),
    eval(e,nconst(m),x) -> nobj(m),
    eval(e,comp(f,g),x) -> eval(e,g,eval(e,f,x)),
    eval(e,tuple(f,g),x) -> pair(eval(e,f,x),eval(e,g,x)),
    eval(e,f,x) = bobj(false) =>
       eval(e,cond(f,g,h),x) -> eval(e,h,x),
    eval(e,f,x) = bobj(true) =>
       eval(e,cond(f,g,h),x) -> eval(e,g,x)
endoftype
complete FP 
noetherian FP 
display FP eval = "_;\_ <_>\"

{***************************************************************************}
{* SOME EXAMPLES FOR EVALUATIONS OF FP-PROGRAMS                            *}
{***************************************************************************}

task  FAC6
  basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT
  unknown x: Obj
  goals   x = eval(declare(
                    emptydecls,
                    'Fac, cond(eqz,
                               nconst(1),
                               comp(tuple(id,comp(p,iconst('Fac))),mu))),
                   comp(s,iconst('Fac)),
                   nobj(5)
                  )
endoftask

task  EVE3
  basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT, BOOL
  unknown x: Obj
  goals   x = eval(declare(declare(
                    emptydecls,
                    'Odd, cond(eqz,
                               bconst(false),
                               comp(p,iconst('Eve)))),
                    'Eve, cond(eqz,
                               bconst(true),
                               comp(p,iconst('Odd)))),
                   iconst('Eve),
                   nobj(3)
                 )
endoftask

task  DUP7
  basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT
  unknown x: Obj
  goals   x = eval(declare(
                    emptydecls,
                    'Dup, cond(eqz,
                               nconst(0),
                               comp(comp(comp(p,iconst('Dup)), s), s))),
                   iconst('Dup),
                   nobj(7)
                 )
endoftask

task  FAC3T2
  basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT
  unknown x: Obj
  goals   x = eval(declare(declare(declare(
                    emptydecls,
                    'Fac, cond(eqz,
                               nconst(1),
                               comp(tuple(id,comp(p,iconst('Fac))),mu))),
                    'Dup, cond(eqz,
                               nconst(0),
                               comp(comp(p,iconst('Dup)),iconst('Ad2)))),
                    'Ad2, comp(s,s)),
                   comp(iconst('Fac),iconst('Dup)),
                   nobj(3)
                 )
endoftask

task  FAC3T2X
  basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT
  unknown dec : Decls, exp : Form, inp, res : Obj
  goals   dec = declare(declare(declare(
                    emptydecls,
                    'Fac, cond(eqz,
                               nconst(1),
                               comp(tuple(id,comp(p,iconst('Fac))),mu))),
                    'Dup, cond(eqz,
                               nconst(0),
                               comp(comp(p,iconst('Dup)),iconst('Ad2)))),
                    'Ad2, comp(s,s)),
          exp = comp(iconst('Fac),iconst('Dup)),
          inp = nobj(3),
          res = eval(dec,exp,inp)
endoftask

{***************************************************************************}
{* SOME GLOBAL DECLARATIONS FOR THE SUBSEQUENT PROOFS                      *}
{***************************************************************************}

type GLOBALS
  basedon DECLARATIONS, OBJECTS
  func d : Decls, y : Obj
endoftype

{***************************************************************************}
{* PROOF OF  f o [g,h] = [f o g, f o h]                                    *}
{***************************************************************************}

task PROOF1
  basedon FP, FORMS, OBJECTS, GLOBALS
  unknown f, g, h : Form
  goals   eval(d,comp(f,tuple(g,h)),y)
            = eval(d,tuple(comp(f,g),comp(f,h)),y)
endoftask

{***************************************************************************}
{* PROOF OF  f o (g o h) = (f o g) o h)                                    *}
{***************************************************************************}

task PROOF2
  basedon FP, FORMS, OBJECTS, GLOBALS
  unknown f, g, h : Form
  goals   eval(d,comp(f,comp(g,h)),y)
            = eval(d,comp(comp(f,g),h),y)
endoftask

{***************************************************************************}
{* PROOF OF A DISTRIBUTIVITY PROPERTY                                      *}
{***************************************************************************}

task PROOF3
  basedon FP, FORMS, OBJECTS, GLOBALS
  unknown f, g, h, k : Form
  goals   eval(d, comp(cond(f,g,h),k),y)
            = eval(d,cond(f,comp(g,k),comp(h,k)),y)
endoftask

{***************************************************************************}
{* A PROOF USING TERM INDUCTION                                            *}
{***************************************************************************}

task PROOF4
  basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT, BOOL
  unknown d: Decls, n : Nat
  goals   d = declare(declare(emptydecls,
              'Odd, cond(eqz,
                         bconst(false),
                         comp(p,iconst('Eve)))),
              'Eve, cond(eqz,
                         bconst(true),
                         comp(p,iconst('Odd)))),
          eval(d,iconst('Eve),nobj(n)) = eval(d,iconst('Odd),nobj(succ(n)))
endoftask

[an error occurred while processing this directive] 31-Jul-2012, 14:17:23 CEST