#use "list.apl". id : name_type. namespace zeta ( nm : name_type. exp : type. type zeta = id\exp. var : id -> exp. obj : [(nm,zeta)] -> exp. sel : exp -> nm -> exp. upd : exp -> nm -> zeta -> exp. func fv exp = [id]. func fvz zeta = [id]. func fvs [(nm,zeta)] = [id]. fv (var X) = [X]. fv (obj L) = fvs L. fv (sel A _) = fv A. fv (upd A _ Z) = L :- List.append (fv A,fvz Z,L). fvz (y\B) = L :- List.remove(y,fv B,L). fvs [] = []. fvs ((_,Z)::L) = L' :- List.append(fvz Z,fvs L, L'). func substz zeta id exp = zeta. func subst exp id exp = exp. func substs [(nm,zeta)] id exp = [(nm,zeta)]. substz (y\B) X C = (y\(subst B X C)) :- y # B, y # C, y # X. subst (var X) X C = C. subst (var Y) X C = (var Y) :- not(Y = X). subst (obj O) X C = obj (substs O X C). subst (sel A L) X C = sel (subst A X C) L. subst (upd A L Z) X C = upd (subst A X C) L (substz Z X C). substs [] X C = []. substs ((N,Z)::O) X C = (N,substz Z X C)::(substs O X C). pred update [(A,B)] A B [(A,B)]. update ((A,_)::L) A B ((A,B)::L). update ((A',B')::L) A B ((A',B')::L') :- A # A', update L A B L'. pred eval exp exp. eval (obj O) (obj O). eval (sel A L) V :- eval A (obj O), List.mem ((L,y\B), O), eval (subst B y (obj O)) V. eval (upd A L Z) (obj O') :- eval A (obj O), update O L Z O'. func t1 = exp. t1 = sel (obj [(l,(x\obj []))]) l. func field_upd exp nm exp = exp. field_upd A L B = upd A L (x\B) :- x # B. ?X = subst (obj [(y,w\var z)]) z (obj []). ). (* From lambda calculus to objects *) namespace lam ( exp : type. var : id -> exp. lam : id\exp -> exp. app : exp -> exp -> exp. ). func do_app zeta.exp zeta.exp = zeta.exp. do_app P Q = zeta.sel (zeta.field_upd P arg Q) val. #open lam. pred trans exp zeta.exp. trans (var X) (zeta.var X). trans (app B A) (do_app B' A') :- trans B B', trans A A'. trans (lam (x\B)) E :- trans B B', E = (zeta.obj [(arg,(x\zeta.sel (zeta.var x) arg)), (val,x\zeta.subst B' x (zeta.sel (zeta.var x) arg))]). ?X = lam (x\var x), trans X Z.