SATySFiで数式を生成する～アッカーマン関数編～

これは2018 SATySFi advent calendar 6日目の記事です。[前] [次]

たとえば話の流れでアッカーマン関数の計算方法の説明が必要になったとき(例1)、手打ちで数式を書きたくはないですよね。何らかの数式処理システムで式を生成して適当な形式でエクスポートするか、スクリプト言語で式を生成するプログラムを書くか検討する所です。

例1. 寿司～虚空編～ (小林銅蟲) 第2話より

f:id:youz:20181204234605j:plain — この後8ページほど数式が続く

しかし2017年人類は高度なデータ表現能力・アルゴリズム記述能力・数式組版能力を併せ持った組版システム“SATySFi”を手に入れました。プログラム生成できるようなタイプの数式ならシュッと生成して美しく組み上げてpdf出力まで出来ちゃいますので、今回はコイツで全部やって行きます。

1. 計算式のデータ表現を作る

まずアッカーマン関数の定義ですが、

f:id:youz:20181205010524p:plain — Wikipediaより

これをSATySFiの関数として書き下すと以下の通り。

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

パターンマッチ構文便利ですね。

ただこれだと普通のint -> int型の関数で、数値を渡して評価すると最終計算結果の数値が返ってくるだけです。今回は計算過程の式が欲しいので、計算式をデータとして表現し、その計算式データを定義通りに変形していく処理を実装する必要があります。

寿司2話に倣って引き算の所は結果の数値のみ書き出す事にすると、計算式に出てくるのは次の2要素のみ。

数値
2引数の関数適用 (引数は数値 or 関数の再帰適用)

数値を葉とした単純な二分木で良さそうですねという事で、計算式データの型は以下のように定義。

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

これで $\operatorname {Ack}(3, 3)$ は Fun(Num(3), Num(3)), $\operatorname {Ack} (2, \operatorname {Ack} (3, 2))$ は Fun(Num(2), Fun(Num(3), Num(2))) のように代数的データ型の値として書けるようになりました。

2. 計算処理の実装

計算式データの計算を1ステップ分進める関数calc1を実装します。

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)

5つのパターンに分けて処理してますが内容は上から順に以下の通り。

数値が渡された時。これ以上計算する物はないのでそのまま返す。
$\operatorname {Ack}(0, n)$ という形の式が渡された時。第2引数に1を加えた数値を返す。
$\operatorname {Ack}(m, 0)$ という形の式が渡された時。式 $\operatorname {Ack}(m - 1, 1)$ を返す。
$\operatorname {Ack}(m, n)$ という形の式が渡された時。式 $\operatorname {Ack} (m - 1, \operatorname {Ack} (m, n - 1))$ を返す。
上記4つ以外、即ち $\operatorname {Ack} (m, \operatorname {Ack} (...))$ という形の式が渡された時。第2引数を1ステップ進めた式に置き換えた式を返す。

パターンマッチと再帰呼出しのおかげでスッキリ書けちゃいますね。念のため正しく計算されてるかを確かめてみましょう。計算式データを文字列化し、display-messageでコンソールに出力します。

...

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

let-inline \test =
  let f e = let () = display-message (aexpr2str e) in calc1 e in
  let _ = Fun(Num(1), Num(1)) |> f |> f |> f |> f |> f |> f in
    {done}

in
document (|
  title = {};
  author = {};
  show-title = false;
  show-toc = false;
|) '<
  +p{\test;}
>

↓コンソール出力

...
 ---- ---- ---- ----
  evaluating texts ...
A(1,1)
A(0,A(1,0))
A(0,A(0,1))
A(0,2)
3
3
  evaluation done.
 ---- ---- ---- ----
...

良さそうですね。あとは渡されたaexpr型データにcalc1を繰り返し適用し、Num(n)に収束するまでの過程をリストに溜め込んで返す関数を作れば計算式生成処理の完成です。

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 []

3. 計算式データを数式(math型データ)に変換する

日本語が紛らわしくなっちゃってますが、この記事では

計算式データ＝ aexpr型データ
数式＝ SATySFiの組版用数式データ (math型データ)

です。生成した計算式データを文書として出力するには、文書中に数式として入れ込まなければなりません。

というわけで今回の数式生成の肝である、計算式データを数式に変換する関数を作ります。

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 \)}

構造は先程テストに使った文字列化関数expr2strとほぼ同じなんですが、こちらはなんやかんやしてmath型データを返すようになっています。

数値の数式化

引数がNum(n)つまり数値の時ですが、int型データnを数式にするにはまず関数arabicで文字列化し、その結果を関数math-charで数式化すればOK。

math-charの第2引数は数式の前後のスペーシングを制御するための“数式クラス”指定で、数値の場合は“通常”を表すMathOrdを使います。

数式クラス指定は他にMathRel, MathBinなど全部で9種類ありますが、詳しく知りたい人はThe SATySFi Bookの10章とLambdaNote社から刊行されている数式組版の2章(図1.)を読むと良いでしょう。

図1. 数式組版 (木枝祐介) 2章より

f:id:youz:20181206010457j:plain — スペーシングの図解

関数適用式の数式化

引数がFun(x, y)の場合ですが、まず引数のxとyをそれぞれ再帰処理で数式データ化しておき、最後に数式リテラル中に埋め込んで返します。

数式中に'#'+'変数名'と書くことで、よくあるスクリプト言語の文字列補間機能のノリで変数に束縛されている数式データを埋め込むことができます。

簡単ですがこれで肝のaexpr型→math型変換は完了。 calc-allで得られた計算式のリストにList.map aexpr2mathを適用すれば組版readyな数式のリストの出来上がり。

4. 数式を並べる

数式のリストが出来たらあとはもう数式用ブロックコマンド+alignに渡してキレイに並べてもらうだけ、だったら良かったんですが、残念ながら+alignはページをまたぐことができないので今回はコマンドを自作。

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}))

これはまあページをまたぐようなネタ数式のためだけのその場しのぎコマンドなので説明は略。普通は+alignコマンドとか使いましょう。

5. 完成

まとめとして、数値2つを渡されたらaexpr型のデータにして2～4の処理を順に適用していく+Ackコマンドを作って完成。

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

+Ack(3)(1);を出力した結果がこちら。 f:id:youz:20181206011339j:plain

ソース全体とpdf → SATySFiでアッカーマン関数

自由にパラメータを変えて遊んでみてください、と言いたい所ですが +Ack(3)(4);はフォントサイズ5pt, 段落マージン1ptの設定でA4用紙185ページほどになります。 Ack(3, 5), Ack(4, 0)くらいまでは大丈夫かもしれませんが、それ以上はまず死ぬと思いますのでご注意ください。

have fun!