i217受講者の大和谷です。
第三回のレポートを提出します。

４つのコードに分かれています。
・問題１のsmlコード
・問題２のCafeObjコード
・問題３の段階１と２のCafeObjコード
・問題３の段階３のCafeObjコード
コードは##############で区切っています。

############################################################################################################

(********************* 問題１ *******************)

(********************** (1) **********************)

(* '='と大小比較を可能とする。 *)
signature TOTALORDER = sig
    eqtype elem;                  (* '='による比較が可能であること。 *)
    val lt : elem * elem -> bool  (* 第一引数が第二引数より「小さい」ならばtrue、それ以外はfalse *)
end;

signature SET =
    sig
	eqtype elem;                       (* 要素の型 *)
        type set;                          (* 集合を表現する型 *)
        val Empty : set                    (* 空の集合 *)
	val element : elem * set -> bool   (* 値が集合に含まれていればtrue *)
	val insert  : elem * set -> set    (* 集合に値を追加する。*)
	val delete  : elem * set -> set    (* 集合から値を取り除く。 *)
    end;

(* 要素の型を表現するストラクチャを引数にとり、集合を表現するストラクチャを生成するファンクタ *)
functor MakeSET(Element : TOTALORDER) : SET =
    struct
	(* 集合を二分木によって実現する。 *)
	
	open Element;                          (* 要素の型elemと大小比較関数ltを取り込む。 *)
	    
	datatype set =
	    Empty                              (* 葉 *)
	  | Node of elem * set * set;          (* 要素と左・右部分木から成る節点 *)
	    
	(* 値が集合に含まれるか検査する。 *)
	fun element (x : elem, Empty) = false
	  | element (x, Node (y, tl, tr)) =
	    if x = y then true
	    else if lt(x,y) then element(x,tl)
		 else  element(x,tr);
		     
	(* 値を集合に挿入する。 *)
	fun insert (x : elem, Empty) = Node(x, Empty, Empty)
	  | insert (x, Node(y, tl, tr)) =
	    if x = y then Node(x, tl, tr) (* 「集合」なので同じ値を重複して保持しない。 *)
	    else if lt(x,y) then Node(y, insert(x,tl), tr)
		 else Node(y, tl, insert(x,tr));
		     
	exception EmptyTree;                   (* 存在しない値の削除を試みた際に発生する例外 *)

	(* 木に含まれる要素のなかで「最小」の要素を取りだし、取り除いた後の木とともに返す。 *)
	fun deletemin Empty = raise EmptyTree
	  | deletemin (Node (y, Empty, tr)) = (y, tr)
	  | deletemin (Node (w, tl, tr)) = (* 最小要素は左部分木に含まれているので左から削除する。 *)
	    let val (y, tl') = deletemin tl
	    in
		(y, Node(w, tl', tr))
	    end;
	    
	(* 値を集合から削除する。 *)
	fun delete (x : elem, Empty) = Empty
	  | delete (x, Node(y, tl, tr)) =
	    if lt(x,y) then Node(y, delete(x,tl), tr)
	    else if lt(y,x) then Node(y, tl, delete(x,tr))
		 else
		     (*
		      「木の頂点の値が、左部分木のあらゆる値より大きく、
		      右部分木のあらゆる値より小さい。」という条件を維持するため、
		      この木に含まれる要素の中でyの次に小さな要素を探しだし、
		      木の新たな頂点に据える。
		      *)
		     if tl = Empty then tr
		     else if tr = Empty then tl
			  else let
				   val (z, tr') = deletemin tr
			       in
				   Node (z, tl, tr')
			       end;
    end;

(********************** (2) **********************)

(* 整数上の全順序を定義する *)
structure Integer : TOTALORDER =
    struct
	type elem = int;
	val lt = op < : (int * int -> bool);
    end;

(* 文字列上の全順序を定義する *)
structure String : TOTALORDER =
    struct
	type elem = string;
	val lt = op < : (string * string -> bool);
    end;

(* 文字列と整数の組での全順序を定義する *)
structure StrIntPair : TOTALORDER =
    struct
	type elem = (string * int);
	fun lt((ls,li):elem, (rs,ri)) =
	    if ls = rs then li < ri
	    else ls < rs;
    end;

(* 各種の集合を定義するストラクチャを生成する *)
structure IntegerSet = MakeSET(Integer);
structure StringSet = MakeSET(String);
structure StrIntPairSet = MakeSET(StrIntPair);

(* リストからセットを生成する。 *)
(* 関数がストラクチャを引数にとれれば、ファンクタで包む必要もない？ *)
functor SetTester(Set : SET) =
    struct
	fun fromList el = foldl (Set.insert) Set.Empty el;
    end;

(************************* テスト ****************************)

print "(********* test for Integer *****************)\n";
Integer.lt(0 , 1) = true;
Integer.lt(1 , 0) = false;
Integer.lt(0 , 0) = false;

print "(********* test for String ******************)\n";
String.lt("aA" , "aB") = true;
String.lt("aB" , "aA") = false;
String.lt("aB" , "aB") = false;

print "(********* test for String Integer pair *****)\n";
StrIntPair.lt(("a",100) , ("b",0)) = true;
StrIntPair.lt(("b",0) , ("a",100)) = false;
StrIntPair.lt(("b",0) , ("b",0)) = false;
StrIntPair.lt(("a",50) , ("a",50)) = false;
StrIntPair.lt(("a",100) , ("a",50)) = false;
StrIntPair.lt(("a",50) , ("a",100)) = true;


print "(************* test for set *****************)\n";
print "(************ using IntegerSet **************)\n";
open IntegerSet;
structure IntegerTester = SetTester(IntegerSet);
open IntegerTester;

print "(*** test for insert ***)\n";
element(1,Empty) = false;                              (* 空集合の確認 *)
element(1,insert(1,Empty)) = true;                     (* 空集合への一要素の挿入 *)
element(2,insert(2,insert(1,Empty))) = true;           (* 頂点より大きな値を挿入 *)
element(0,insert(2,insert(1,Empty))) = false;          (* 存在しない値 *)
element(0,insert(0,insert(1,Empty))) = true;           (* 頂点より小さな値を挿入 *)
element(2,insert(0,insert(1,Empty))) = false;          (* 存在しない値 *)
element(0,insert(2,insert(0,insert(1,Empty)))) = true; (* 左右いずれも空ではない場合 *)
element(1,insert(2,insert(0,insert(1,Empty)))) = true; 
element(2,insert(2,insert(0,insert(1,Empty)))) = true;
element(3,insert(2,insert(0,insert(1,Empty)))) = false;(* 存在しない値 *)
element(2,insert(2,insert(2,insert(0,insert(1,Empty))))) = true;(* 重複する値 *)

print "(*** test for delete ***)\n";
element(1,delete(1,fromList[1])) = false;          (* 唯一の要素を削除 *)
element(2,delete(2,fromList[1])) = false;          (* 含まれない値の削除を試みる。 *)
element(0,delete(0,fromList[1,0])) = false; (* 最小要素の削除 *)
element(1,delete(1,fromList[1,0,2])) = false; (* 木の根の削除 *)
element(2,delete(2,fromList[1,0,2])) = false; (* 最大要素の削除 *)
element(1,delete(2,fromList[1,0,2])) = true; (* 削除されない要素の保存確認 *)

(*
 ここまでで、String,Integer,StrIntPairと、
 Integerを引数に与えた場合のMakeSETファンクタの動作が確認された。
 MakeSETファンクタは、引数に与えられたストラクチャがTOTALORDERの仕様通りに動作する限り
 正しく動作する。
 よって、StringSet,StrIntPairSetのテストは行わない。
 *)

############################################################################################################
-- i217 report 3 - 2
-- YAMATODANI Kiyoshi (ID : 010119)

-- proof score of equivalence of two functions

-- specification of list
mod! LIST (X :: TRIV) {

  [ List ]

  op nil : -> List
  op _$_ : Elt List -> List
  op _@_ : List List -> List { assoc }

  -- '@' has nil as identity (but if specify 'id:nil' in above op statement,infinite loop.)
  eq nil @ L:List = L .
  eq L:List @ nil = L .

  eq (E:Elt $ L1:List) @ L2:List = (E $ (L1 @ L2)) .
}

-- specification of two functions which reverse list
mod! REVERSE (X :: TRIV) {
  protecting(LIST(X))

  -- reverse function
  op rev : List -> List
  eq rev(nil) = nil .
  eq rev(x:Elt $ xs:List) = rev(xs) @ (x $ nil) .

  -- another reverse function
  op revi : List List -> List
  eq revi(nil,ys:List) = ys .
  eq revi((x:Elt $ xs:List),ys:List) = revi(xs,x $ ys) .
}

-- proof of equivalence of rev and revi
-- for all list xs and all list ys , revi(xs,ys) = rev(xs) @ ys
open REVERSE

set trace whole on
-- x and xs are constant , because x and xs are fixed in each step of induction .
op x : -> Elt .
ops xs : -> List .

--> base case
red revi(nil , ys:List) == rev(nil) @ ys .

--> induction hypothesis
eq revi(xs , ys:List) = rev(xs) @ ys .
--> conclusion
red revi((x $ xs) , ys:List) == rev(x $ xs) @ ys .

close

eof

############################################################################################################
-- -*- Mode:CafeOBJ -*-

-- i217 report 3 - 3 - (1) & (2)
-- YAMATODANI Kiyoshi (ID : 010119)

--> binary operation symbols
mod! OPsym {
  [ Opsym ]
  ops ++ -- x / ee : -> Opsym
}

--> value
mod! VAL {
  protecting(INT)
  [ Int Bool < Val ]
}

--> expressions 
mod! Aexp {
  protecting(OPsym + VAL)
  -- Val is Exp
  [ Val < Exp ]

  --> arithmatic operations
  op (_ _ _)  : Exp Opsym Exp -> Exp
    
    --> if expression
  op (if(_,_,_)) : Exp Exp Exp -> Exp
}

--> application of arithmetic operations
mod! APPop { 
  extending(Aexp) 

  op apply_to_ _ : Opsym Exp Exp -> Val

  --> arithmetic operation
  eq apply ++ to I:Int J:Int = I + J .
  eq apply -- to I:Int J:Int = I - J .
  eq apply x to I:Int J:Int = I * J .
  eq apply / to I:Int J:NzInt = I quo J .

  --> compare
  eq apply ee to I:Int J:Int = I == J .
}

--> evaluator/reducer
mod! EVAL { 
  protecting(APPop)

  --> evaluation operation
  op eval : Exp -> Val

  --> variable declaration
  vars E E1 E2 E3 : Exp

  --> base cases: [ Bool Int < Exp ] 
  eq eval(I:Int) = I .
  eq eval(B:Bool) = B .

  --> op (_ _ _)  : Exp Opsym Exp -> Aexp
  eq eval(E1 Op:Opsym E2) = apply Op to eval(E1) eval(E2) .

  --> if(_ _ _) : Exp Exp Exp -> Exp
  ceq eval(if(E1,E2,E3)) = eval(E2) if eval(E1) == true .
  ceq eval(if(E1,E2,E3)) = eval(E3) if eval(E1) == false .

}

--> test case for if exp
--> should be 2
red in EVAL : eval (if((1 ee 2), 1, 2)) .
--> should be 4
red in EVAL : eval (if((1 ee 1), 4, 5)) .
--> should be 50
red in EVAL : eval ((3 ++ 2) x (((3 / 2) x if((3 ee if(((3 -- 2) ee 2), 2, 3)), 10, 4)))) .

**  *********************************************************
**> definition of Abstract Machines for running compiled code
**  *********************************************************

--> parameterized list
mod! LIST (ELT :: TRIV) {
  protecting(INT)
  [ List ]
  op nil : -> List
  --> cons
  op (_&_): Elt List -> List

  --> append
  op (_@_) : List List -> List
  eq nil @ L:List = L .
  eq L:List @ nil = L .

  eq (E:Elt & L:List) @ L1:List = E & (L @ L1) .

  --> the following equation holds
  --> this can be proved by induction on the length of list
  eq (L1:List @ L2:List) @ L3:List = L1 @ (L2 @ L3) .

  --> count of elements contained in list
  op length : List -> Int
  eq length(nil) = 0 .
  eq length(E:Elt & L:List) = 1 + length(L) .

  --> drop first i elemtn from list
  op drop : List Int -> List
  eq drop(L:List, 0) = L .
  ceq drop((E:Elt & L:List), n:Int) = drop(L, (n - 1)) if n > 0 .
--  eq drop(L:List, length(L)) = nil .
  eq drop(L:List @ M:List, length(L)) = M .
  eq drop(L:List @ (E:Elt & M:List), length(L) + 1) = M . -- ad hoc...
}

--> preliminary dummy Item which will be refined later
mod* ITEM { [ Item ] }

--> list of the preliminary items
make ITL (LIST(ITEM {sort Elt -> Item})
           * {sort List -> ItemList})

--> instructions
mod! INST {
  protecting(OPsym + INT)  

  -- instructions
  [ Inst ]
  op Load_ : Int -> Inst
  op Load_ : Bool -> Inst
  op Apply_ : Opsym  -> Inst
  op Jump_ : Int -> Inst  -- unconditional jump . skip n insts
  op FJump_ : Int -> Inst -- conditional jump .if stack top is false,skip n insts
}

--> list of items 
--  this item list structure is needed to handle if-expression
--  but not necessary for arithmetic expression
mod! ITEMlist {
  protecting(INST)
  using(2TUPLE(ITL{sort Elt -> ItemList},
               ITL{sort Elt -> ItemList}) 
              * {sort 2Tuple -> Itl2Tuple})
  [ Inst Itl2Tuple < Item ]
}

-- [ Int < Val < Exp ]
--> value stack
make VALstack (LIST(VAL {sort Elt -> Val}) 
               * {sort List -> ValStack})

--> abstract machine for executing/running 
--> the binary operations and if expressions on integers
mod! ABSmachine {
  protecting (APPop) 
  protecting (2TUPLE(ITEMlist{sort Elt -> ItemList},
                     VALstack{sort Elt -> ValStack})
               * {sort 2Tuple -> Config})

  --> exec: execution
  op exec_on_ : Inst Config -> Config 
  eq exec (Load I:Int) on 
      << ITL:ItemList ; VS:ValStack >> = 
      << ITL ; (I & VS) >> .
  eq exec (Load B:Bool) on 
      << ITL:ItemList ; VS:ValStack >> = 
      << ITL ; (B & VS) >> .

  eq exec (Apply Op:Opsym) on 
    << ITL:ItemList ; (V1:Val & V2:Val & VS:ValStack) >> = 
      << ITL ; (apply Op to V2 V1) & VS >> .

  --> unconditional jump
  eq exec (Jump n:Int) on
    << ITL:ItemList ; VS:ValStack >> = << drop(ITL,n) ; VS >> .

  --> conditional jump
  ceq exec (FJump n:Int) on
    << ITL:ItemList ; (B1:Bool & VS:ValStack) >> = << drop(ITL,n) ; VS >> if B1 == false .
  ceq exec (FJump n:Int) on
    << ITL:ItemList ; (B1:Bool & VS:ValStack) >> =  << ITL ; VS >> if B1 == true .

  --> run
  op run_ : Config -> Config
  eq run << nil ; VS:ValStack >> = << nil ; VS:ValStack >> .
  eq run << IS:Inst & ITL:ItemList ; VS:ValStack >> = 
    run (exec IS on << ITL:ItemList ; VS:ValStack >>) .

}

mod! COMPILER {
  protecting (Aexp + ITEMlist)

  op compile_ : Exp -> ItemList

  eq compile I:Int = (Load I) & (nil):ItemList .
  eq compile B:Bool = (Load B) & (nil):ItemList .

  eq compile (E1:Exp Op:Opsym E2:Exp) = 
      compile(E1) @ (compile(E2) @ ((Apply Op) & (nil):ItemList)) .

  -- translate 'if' expression to conditional jump
  eq compile (if(E1:Exp,E2:Exp,E3:Exp)) =
    ((compile(E1) @
      (FJump (length(compile(E2)) + 1) & compile(E2))) @
	(Jump (length(compile(E3))) & compile(E3))) .
}

--> **********
--> test cases
--> **********
--> should be 9
red in (ABSmachine + COMPILER) : run << compile ((5 ++ ((33 -- 22) x 2)) / 3)  ; (nil):ValStack >> .
--> should be 2
red in (ABSmachine + COMPILER) : run << compile (1 ++ if((1 ee 1), 1, 2)) ; (nil):ValStack >> .
--> should be 4
red in (ABSmachine + COMPILER) : run << compile (if((1 ee 1), 4, 5)) ; (nil):ValStack >> .
--> should be 50
red in (ABSmachine + COMPILER) : run << compile ((3 ++ 2) x (((3 / 2) x if((3 ee if(((3 -- 2) ee 2), 2, 3)), 10, 4)))) ; (nil):ValStack >> .



--> **************************************************************
-->     Verification of Correctness of If-Expession Compiler
--> **************************************************************

open (EVAL + ABSmachine + COMPILER) 

--> declarations of variables
--  (do not use all the variables declared)
vars ITL ITL1 ITL2 ITL3 : ItemList .
vars VS VS1 : ValStack .
vars I I1 I2 : Int .
vars E E1 E2 : Exp .
vars OP OP1 : Opsym .
--> end of variable definitions

-- red run << compile(I) @ ITL ; VS >> .
-- red << ITL ; (eval(I) & VS) >> .

--> induction base
--> for Int
red run << compile(I) @ ITL ; VS >> == run << ITL ; (eval(I) & VS) >> .
**> should be true

--> induction hypothesis
ops e1 e2 e3 : -> Exp .
eq run << (compile(e1) @ ITL) ; VS >> = run << ITL ; (eval(e1) & VS) >> .
eq run << (compile(e2) @ ITL) ; VS >> = run << ITL ; (eval(e2) & VS) >> .
eq run << (compile(e3) @ ITL) ; VS >> = run << ITL ; (eval(e3) & VS) >> .

--> induction step for arithmetic expressions
-- red run << compile(e1 OP e2) @ ITL ; VS >> .
-- red run << ITL ; (eval(e1 OP e2) & VS) >> .
red run << compile(e1 OP e2) @ ITL ; VS >> 
				     == run << ITL ; (eval(e1 OP e2) & VS) >> .
**> should be true

--> 'if' expression has two case. condition is true and condition is false .

--> induction step for if expressions (case 1 : condition evals true)
-- red run << compile(if(true,e2,e3)) @ ITL ; VS >> .
-- red run << ITL ; (eval(if(true,e2,e3))) & VS >> .
red run << compile(if(true,e2,e3)) @ ITL ; VS >>
				     == run << ITL ; (eval(if(true,e2,e3))) & VS >> .
**> should be true

--> induction step for if expressions (case 1 : condition evals false)
-- red run << compile(if(false,e2,e3)) @ ITL ; VS >> .
-- red run << ITL ; (eval(if(false,e2,e3))) & VS >> .
red run << compile(if(false,e2,e3)) @ ITL ; VS >> 
				     == run << ITL ; (eval(if(false,e2,e3))) & VS >> .
**> should be true

-- ****************************************
--> We have proven what we wanted to prove!
-- ****************************************

close

eof
############################################################################################################
-- -*- Mode:CafeOBJ -*-

-- i217 report 3 - 3 - (3)
-- YAMATODANI Kiyoshi (ID : 010119)

-- BUG
-- 1. cannot express addition of two variable
-- "x" ++ "y"  ==> ambiguous , because STRING module define string addition operator '++' .

-- add fix operator into interpreter

--> binary operation symbols
mod! OPsym {
  [ Opsym ]
  ops ++ -- x / ee : -> Opsym
}

--> value
mod! VAL {
  protecting(INT)
  protecting(STRING)
  [ Int Bool String < Val ]
}

--> expressions 
mod! Aexp {
  protecting(OPsym + VAL + STRING)
  -- Val is Exp
  [ Val < Exp ]

  --> arithmatic operations
  op (_ _ _)  : Exp Opsym Exp -> Exp
    
    --> if expression
  op (if(_,_,_)) : Exp Exp Exp -> Exp

    --> lambda expression
  op fn_=>_ : String Exp -> Exp

    --> function apply
  op app_ _ : Exp Exp -> Exp

    --> fix operator
  op fix_ : Exp -> Exp
}

mod! LIST (ELT :: TRIV) {
  [ List ]
  op nil : -> List
    --> cons
  op (_&_): Elt List -> List

    --> append
  op (_@_) : List List -> List
  eq nil @ L:List = L .

  eq (E:Elt & L:List) @ L1:List = E & (L @ L1) .

  --> the following equation holds
  --> this can be proved by induction on the length of list
  eq (L1:List @ L2:List) @ L3:List = L1 @ (L2 @ L3) .

}

--> mapping variable name to expression
mod! ENVENTRY {
  protecting(STRING)
  using (2TUPLE(STRING{sort Elt -> String},
		Aexp{sort Elt -> Exp})
               * {sort 2Tuple -> EnvEntry})
  [ EnvEntry ]
}

--> list of ENVENTRY
mod! ENV {
  protecting(Aexp)
  protecting(ENVENTRY)
  protecting(LIST(ENVENTRY {sort Elt -> EnvEntry})
	      * {sort List -> Env})

  op Empty : -> Env
    --> retrieve mapped expression
  op lookup : Env String -> Exp
    --> add entry to environment
  op register : Env String Exp -> Env

    -- not considered case where name is not found .
  ceq lookup((<< n:String ; e:Exp >> & others:Env), t:String) = e if n == t .
  ceq lookup((<< n:String ; e:Exp >> & others:Env), t:String) = lookup(others,t) if (n == t) == false .

  eq register(env:Env,n:String,e:Exp) = << n ; e >> & env .
}

--> application of arithmetic operations
mod! APPop { 
  extending(Aexp) 

  op apply_to_ _ : Opsym Exp Exp -> Val

  --> arithmetic operation
  eq apply ++ to I:Int J:Int = I + J .
  eq apply -- to I:Int J:Int = I - J .
  eq apply x to I:Int J:Int = I * J .
  eq apply / to I:Int J:NzInt = I quo J .

  --> compare
  eq apply ee to I:Int J:Int = I == J .
}

--> evaluator/reducer
mod! EVAL { 
  protecting(APPop)
  protecting(ENV)

  --> evaluation operation
  op eval : Env Exp -> Val
  op subst : Env Exp -> Exp

  --> variable declaration
  vars E E1 E2 E3 : Exp

  --> substitute value registered in env for variable name 
  eq subst(E:Env,I:Int) = I .
  eq subst(E:Env,B:Bool) = B .
  eq subst(E:Env,V:String) = lookup(E,V) .
  eq subst(E:Env,(E1 Op:Opsym E2)) = subst(E,E1) Op subst(E,E2) .
  eq subst(E:Env,if(E1,E2,E3)) = if(subst(E,E1),subst(E,E2),subst(E,E3)) .
  eq subst(E:Env,app E1 E2) = app subst(E,E1) subst(E,E2) .
  eq subst(E:Env,fn (V:String) => (B:Exp)) =
    (fn V => (subst(register(E,V,V),B))) . -- mask outer binding by parameter variable
  eq subst(E:Env,fix (F:Exp)) = fix (subst(E,F)) .

  --> base cases: [ Bool Int < Exp ] 
  eq eval(E:Env,I:Int) = I .
  eq eval(E:Env,B:Bool) = B .
  eq eval(E:Env,V:String) = eval(E, lookup(E,V)) .
  eq eval(E:Env,fn (V:String) => (B:Exp)) = (fn V => (subst(register(E,V,V),B))) . -- function as value
  eq eval(E:Env,fix (F:Exp)) = fix (subst(E,F)) .

  --> op (_ _ _)  : Exp Opsym Exp -> Aexp
  eq eval(E:Env,E1 Op:Opsym E2) = apply Op to eval(E,E1) eval(E,E2) .

  --> if(_,_,_) : Exp Exp Exp -> Exp
  ceq eval(E:Env,if(E1,E2,E3)) = eval(E,E2) if eval(E,E1) == true .
  ceq eval(E:Env,if(E1,E2,E3)) = eval(E,E3) if eval(E,E1) == false .

  --> app((fn v => body) arg)
  eq eval(E:Env,app (fn (V:String) => (B:Exp)) (A:Exp)) = eval(register(E,V,A) , B) .
  -- if first argument of app is not 'fn' expression, it may eval to 'fn' expression .
  eq eval(E:Env,app (app E1 E2) E3) = eval(E,app (eval(E,app E1 E2)) E3) .
  eq eval(E:Env,app (fix E1) E2) = eval(E,app (app (eval(E,E1)) (fix E1)) (eval(E,E2))) .
  eq eval(E:Env,app V:String E2) = eval(E,app (eval(E,V)) (eval(E,E2))) .
}

--> test case
--> if expression
red in EVAL : eval (Empty,if((1 ee 2), 1, 2)) .
red in EVAL : eval (Empty,if((1 ee 1), 4, 5)) .
red in EVAL : eval (Empty,(3 ++ 2) x (((3 / 2) x if((3 ee if(((3 -- 2) ee 2), 2, 3)), 10, 4)))) .
--> function value
red in EVAL : eval (Empty,fn "x" => ("x" ++ 1)) .
--> apply function to expression
red in EVAL : eval (Empty,(app (fn "x" => ("x" ++ 1)) 1)) . 
red in EVAL : eval (Empty,(app (fn "x" => (fn "y" => ("x" ++ 10))) 1)) . -- rsult is another function
red in EVAL : eval (Empty,(app (app (fn "x" => (fn "y" => ("x" ++ 10))) 1) 2)) .

--> fix operator
red in EVAL : eval (Empty,fix (fn "x" => (if(("x" ee 0), 1, 2)))) .
--> factorial ???
red in EVAL : eval (Empty,fix (fn "f" => (fn "x" => (if(("x" ee 0), 1, ("x" x (app "f" ("x" -- 1)))))))) .
--> 4! = 24
red in EVAL : eval (Empty,app (fix (fn "f" => (fn "x" => if(("x" ee 0), 1, ("x" x (app "f" ("x" -- 1))))))) 4) .
--> 5 x (((3/2) x 4) + 4!) = 140 ???
red in EVAL : eval (Empty,(5 x (((3 / 2) x if((3 ee 2), 10, 4))
				++
				  (app
				     (fix (fn "f" =>
					     (fn "x" => if(("x" ee 0), 1, ("x" x (app "f" ("x" -- 1)))))))
				   4)))) .
eof
############################################################################################################
以上です。