[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