SATySFiでラムダ計算

lambdacalc.pdf

lambdacalc.saty

@require: stdja
@require: list
@require: math
@require: option

% ref. http://www.kb.ecei.tohoku.ac.jp/~sumii/class/keisanki-software-kougaku-2005/lambda.pdf

type exp =
  | Var of string * int
  | Abs of exp * exp
  | App of exp * exp

let vareq x y =
  match (x, y) with
  | (Var(s, i), Var(t, j)) -> string-same s t && i == j
  | _ -> false

let-rec allvar
  | ((Var _) as v) = [v]
  | (Abs(x, e))    = x :: (allvar e)
  | (App(x, y))    = List.append (allvar x) (allvar y)

let-rec find eq x l =
  match l with
  | []     -> None
  | e :: r -> if eq x e then Some(e) else find eq x r

let dedup eq l =
  List.fold-left (fun a e -> (
    match find eq e a with
    | None   -> e :: a
    | Some _ -> a
  )) [] l

let-mutable sym-counter <- -1
let-mutable sym-used <- []

let-rec gensym () =
  let () =  sym-counter <- !sym-counter + 1 in
  let c = string-unexplode [!sym-counter mod 26 + 97] in
  let p = !sym-counter / 26 in
  let v = Var(c, p) in
    match find vareq v !sym-used with
    | None   -> v
    | Some _ -> gensym ()

let-rec subst e2 x e1 =
  match e1 with
  | Var(_) -> if vareq x e1 then e2 else e1
  | Abs(y, e) ->
    let y2 = gensym () in
      Abs(y2, subst e2 x (subst y2 y e))
  | App(e, f) ->
    App(subst e2 x e, subst e2 x f)

let-rec step e =
  match e with
  | Var(x) -> None
  | Abs(x, e0) -> (
    match step e0 with
    | None -> None
    | Some(e) -> Some(Abs(x, e))
    )
  | App(e1, e2) -> (
    match e1 with
    | Abs(x, e0) -> Some(subst e2 x e0)
    | _ -> (
      match step e1 with
      | Some(e) -> Some(App(e, e2))
      | None -> (
        match step e2 with
        | Some(e) -> Some(App(e1, e))
        | None -> None
      )))

let reduct-all e lim =
  let-rec r e a i =
    if i > lim then
      List.reverse (e :: a)
    else 
      match step e with
      | None -> List.reverse (e :: a)
      | Some(f) -> r f (e :: a) (i + 1)
  in
    r e [] 0

let-rec repeat-string
  | s 0 = ` `
  | s n = s ^ (repeat-string s (n - 1))

let-rec exp2math
  | (Var(x, i)) =
    let p = math-char MathOrd (repeat-string `′` i) in
      ${\mathit-token!(x)#p}
  | (Abs(x, e)) =
    let mx = exp2math x in
    let me = exp2math e in
      ${\lambda #mx . #me}
  | (App(x, y)) =
    let mx = exp2math x in
    let px = match x with
      | Var _         -> mx
      | App(_, Var _) -> mx
      | _ -> ${\(#mx\)}
    in
    let my = exp2math y in
    let py = match y with
      | Var _ -> my
      | _     -> ${\(#my\)}
    in
      math-concat px py

let-block ctx +lambdacalc lm lexp =
  let () = sym-counter <- -1 in
  let () = sym-used <- (dedup vareq (allvar lexp)) in
  let (f::r) = reduct-all lexp 100 |> List.map exp2math in
  let ml = [lm; ${= #f}] :: (List.map (fun m -> [${}; ${\to #m}]) r) in
    read-block ctx '<+align(ml);>

let var s = Var(s, 0)
let abs v e = Abs(v, e)
let app e1 e2 = App(e1, e2)

let cnum n =
  let f = var `f` in
  let x = var `x` in
  let-rec r
    | 0 a = a
    | i a = r (i - 1) (app f a)
  in
    abs f (abs x (r n x))

% pred = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
let pred =
  let f = var `f` in
  let g = var `g` in
  let h = var `h` in
  let n = var `n` in
  let u = var `u` in
  let x = var `x` in
    abs n (abs f (abs x (app (app (app n (abs g (abs h (app h (app g f))))) (abs u x)) (abs u u))))

in
document (|
  title = {\SATySFi;でλ計算};
  author = {youz};
  show-title = false;
  show-toc = false;
|) '<
  +lambdacalc(${3^2})(app (cnum 2) (cnum 3));
  +lambdacalc(${\text!({pred})\ 3})(app pred (cnum 3));
>