SATySFiでアッカーマン関数

ack-3-1.pdf

ack.saty

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

let-rec ack
  | 0 n = n + 1
  | m 0 = ack (m - 1) 1
  | m n = ack (m - 1) (ack m (n - 1))

type aexpr =
  | Num of int
  | Fun of aexpr * aexpr

let-rec calc1
  | (Num(n))              = Num(n)
  | (Fun(Num(0), Num(n))) = Num(n + 1)
  | (Fun(Num(m), Num(0))) = Fun(Num(m - 1), Num(1))
  | (Fun(Num(m), Num(n))) = Fun(Num(m - 1), Fun(Num(m), Num(n - 1)))
  | (Fun(x, y))           = Fun(x, calc1(y))

let calc-all e0 =
  let-rec repeat e a =
    match e with
    | Num(_) -> List.reverse (e :: a)
    | _      -> repeat (calc1 e) (e :: a)
  in
    repeat e0 []

let-rec aexpr2str
  | (Num(n))    = (arabic n)
  | (Fun(x, y)) = `A(` ^ (aexpr2str x) ^ `,` ^ (aexpr2str y) ^ `)`

let-rec expr2math
  | (Num(n))    = math-char MathOrd (arabic n)
  | (Fun(x, y)) =
    let x = expr2math x in
    let y = expr2math y in
      ${A\( #x, #y \)}

let-block ctx +eqns mlst =
  let em = embed-math ctx in
  let print ib = line-break true true ctx (ib ++ inline-fil) in
  match mlst with
  | []        -> block-nil
  | f::[]     -> print (em f)
  | f::(s::r) ->
    let margin = match space-between-maths ctx f ${=} with
      | None       -> inline-nil
      | Some(ibsp) -> ibsp
    in
    let indent = inline-skip (get-natural-width (em f)) ++ margin in
    let p m = print (indent ++ (em ${= #m})) in
      List.map p r
      |> List.fold-left (+++) (print (em ${#f = #s}))

let-block ctx +Ack m n =
  let ms = Fun(Num(m), Num(n))
         |> calc-all
         |> List.map expr2math
  in
    read-block ctx '<+eqns(ms);>

let-block ctx +ctx conf bt =
  let c = List.fold-left (fun c f -> f c) ctx conf in
    read-block c bt

in
document (|
  title = {Ackermann function};
  author = {youz};
  show-title = false;
  show-toc = false;
|) '<
  +ctx[
    set-paragraph-margin 8pt 8pt
  ] <
    +Ack(3)(1);
  >
>