(datatype lambda-expr if (not (= X lambda)) X : symbol; ______________ X : lambda-expr; X : lambda-expr; Y : lambda-expr; ========================= [X Y] : lambda-expr; if (not (= X lambda)) X : symbol; Y : lambda-expr; ===================== [lambda X Y] : lambda-expr;) (define aor {lambda-expr --> lambda-expr} [lambda V [E V]] -> E where (not (free? V E)) [lambda X Y] -> [lambda X (aor Y)] [[lambda X Y] Z] -> (let Alpha (alpha [lambda X Y]) (aor (beta Alpha (aor Z)))) [X Y] -> (let AOR (type [(aor X) (aor Y)] lambda-expr) (if (= AOR [X Y]) AOR (aor AOR))) X -> X) (define free? {lambda-expr --> lambda-expr --> boolean} V V -> true V [lambda V _] -> false V [lambda _ Y] -> (free? V Y) V [X Y] -> (or (free? V X) (free? V Y)) _ _ -> false) (define alpha {lambda-expr --> lambda-expr} [lambda X Y] -> (let V (gensym x) [lambda V (replace X (alpha Y) V)]) [X Y] -> [(alpha X) (alpha Y)] X -> X) (define beta {lambda-expr --> lambda-expr --> lambda-expr} [lambda X Y] Z -> (replace X Y Z)) (define replace {lambda-expr --> lambda-expr --> lambda-expr --> lambda-expr} X [lambda X Y] _ -> [lambda X Y] X X Z -> Z X [Y Y*] Z -> [(replace X Y Z) (replace X Y* Z)] X [lambda Y Y*] Z -> [lambda Y (replace X Y* Z)] _ Y _ -> Y)