最近 satysfi-derive というライブラリを Satyrographos で公開しました。もともと satysfi-base の一部だったものを独立したライブラリとして切り分けたものになります。機能としてはsatysfi-baseの一部だった頃(当時の記事)からあまり変わっていないのですが、細かい部分がアップデートされているため新しく紹介記事を書いています。

これは何？

satysfi-derive は組版処理システム SATySFi で導出木を書くためのコマンドとDSLを提供するライブラリです。SATySFi 及び LaTeX の既存のライブラリと比較して以下の点を特徴とします。

可読性の高いDSLで導出木を書ける
組版の設定を柔軟に変更できる
回帰テストでコードの品質を担保している

例えば以下のコードをコンパイルすると

@require: math
@require: base/typeset/satysfi-it
@require: derive/derive

open Derive in
satysfi-it ${
  \proven!(
    open DeriveDSL in
    derive ${ \vdash A \wedge \paren {B \vee C} }
    |> by { ${\wedge} I }
    |> from [
        assume ${ \vdash A };
        derive ${ \vdash B \vee C }
        |> by { ${\vee} I }
        |> from [
          assume ${ \vdash B };
        ];
    ]
  )
}

以下のような導出木が描画されます。

インストール方法

Satyrographos でインストールできます。

$ opam install satysfi-derive
$ satyrogaraphos install -l derive

使い方

導出木を書く

satysfi-derive 関連のモジュールを使用するためには @require derive/derive をファイルの先頭に書いてください。

導出木を描画するためには数式モード中で \Derive.proven コマンドを使います。コードの最初の方でDeriveモジュールをopenしておくと単に\provenと書くことができます。

% 数式モード
\proven!(derivation)

(!(...)は数式モードからプログラムモードへ切り替えるための構文です。)

ここで引数の derivation は導出木の内容を表すDeriveAst.t型の値です。DeriveAst.tの値を構築するためのDSLをDeriveDSLモジュールが提供しているのでこれを使いましょう。DeriveDSLが提供している関数は以下の通りです。

derive
from
assume
by
byOp
withLine

導出木をつくる

derive が一番基本的な関数で、derive ${math}で前提部が空で結論部が${math}の導出木を構築します。基本的に導出木を構築する際にはderiveから始めることになると思います。

deriveの使用例

derive ${A \wedge B}

前提を設定する

derivation |> from [derivation1; derivation2; ...]はderivationの前提部をderivation1, derivation2...それぞれに対応する導出木に設定します。

fromの使用例

derive ${A \wedge B}
|> from [
  derive ${A};
  derive ${B};
]

仮定をつくる

assume は derive の亜種で、deriveが実線を描画していたのに対してassumeは線を描画しません。ある導出木が仮定である場合はassumeを使った方が適切でしょう。

assumeの使用例

derive ${A \wedge B}
|> from [
  assume ${A};
  assume ${B};
]

ラベルの設定

derivation |> by {label} は導出木のラベルを設定します。

byの使用例

derive ${A \wedge B}
|> by {${\wedge}-intro}
|> from [
  assume ${A};
  assume ${B};
]

derivation |> byOp {label} も導出木のラベルを設定しますが、ラベルの表示場所がbyと反対側になります。

byOpの使用例

derive ${A \wedge B}
|> by {${\wedge}-intro}
|> byOp {(1)}
|> from [
  assume ${A};
  assume ${B};
]

線の変更

derivation |> withLine line は導出の線がどのように描画されるかを明示的に設定します。lineにはDeriveLine.t型の値が使えますが、DeriveDSLで用意されているものは以下の三つです。

standard-line: 実線
no-line: 線なし
dotted-line dot-len spacing: 点線(点の長さがdot-len、空白の長さがspacing)

standard-lineとno-lineはderiveとassumeでそれぞれデフォルトで使われているので、withLineを使うのはdotted-lineを使いたい場合になるでしょう。他の線を自前で定義したい場合には DeriveLine.make (ドキュメント) を使うことを検討してください。

withLineの使用例

derive ${A \wedge B}
|> withLine (dotted-line 2pt 1pt)

レイアウトを調整する

DeriveConfig モジュール(ソースコード)を使うことで細かいレイアウトを調整することができます。具体的には以下のプロパティを調整することが可能です。

main-label-position: byでラベルがどちら側に配置されるか
default-line: deriveで使われる線
line-vertical-margin: 下図の1。線と結論・前提との間。
line-horizontal-margin: 下図の2。線と左右のラベルとの間。
assumption-spacing: 下図の3。前提同士の間。
line-thickness: 下図の4。線の厚さ。
content-padding: 下図の5。結論部と前提部のパディング(線の長さに影響します)

特に設定をしなければ DeriveConfig.defaultがデフォルトの設定として使われます。自前の設定を使いたい際には\provenのオプショナル引数を用いてください。

DeriveConfigの使用例

open Derive in
let my-derive-config = open DeriveConfig in
    default
    |> set-main-label-position LabelRight
    |> set-default-line (DeriveLine.dotted-line 5pt 5pt)
    |> set-line-vertical-margin 10pt
    |> set-line-horizontal-margin 10pt
    |> set-bar-thickness 10pt
    |> set-assumption-spacing 30pt
in
...
${
  \proven ?:!(my-derive-config) !(
    open DeriveDSL in
    derive ${ \Gamma \vdash \Delta }
    |> by {Cut}
    |> from [
      assume ${\Gamma \vdash \Delta, A};
      assume ${\Gamma, A \vdash \Delta}
    ]
  )
}

まとめと宣伝

以上がsatysfi-deriveの紹介です。我ながら便利なものを作れたと思っているので、ドシドシ使ってフィードバックをもらえると嬉しいです。要望等があれば Issue を立ててください。

ところで私の所属している同人誌サークル yabaitech.tokyo が技術書典10で新刊 yabaitech.tokyo vol.6 を販売中です。興味があれば買っていただけると嬉しいです！既刊のyabaitech.tokyo vol.3の「真矛盾主義入門」では実際に導出木を satysfi-derive (の前身のコード) を用いて導出木を組版しています。こちらも興味があれば是非🙇

それでは皆さん、快適なSATySFiライフを楽しんでください👋