SATySFiで導出木を書くDSLをつくった

⚠ この記事は最新の機能を反映していません。[SATySFi の導出木描画ライブラリ satysfi-derive](https://qiita.com/zptmtr/items/5f64e11c13b677b9f665) を参照してください。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/5a5b841c-d15b-311b-a5fe-6f3d9d5691b0.png)
**ひとこと:** ↑こういう導出木が↓こういう感じのコードで書けるようになる

    \proven!(
      open DeriveDSL in
      derive ${ \biseq{a}{b}{c}{d, A} }
      |> by {(Cut P)}
      |> from [
          derive ${ \biseq{a}{b}{c, A}{d, A} }
          |> by {(Weakening)}
          |> from [
              derive ${ \biseq{\void}{\void}{A}{A} }
              |> by {(Reflexivity R)}
          ];
          derive ${ \biseq{a, A}{b}{c}{d, A} }
          |> by {(Weakening)}
          |> from [
              assume ${ \biseq{a, A}{b}{c}{d} }
          ]
      ]
    )


証明論や型システムについての記事を書いていると、しばしば導出木を書く必要がでてきます。Latexだと [bussproof](https://ctan.org/pkg/bussproofs) あたりがよく使われている気がします。bussproof は組版の品質は上々なんですが、導出木の記述に独自のスタック指向のDSLを使っていて、読んだり変更を加えたりするのが少々面倒くさかったりします。

そこで [SATySFi](https://github.com/gfngfn/SATySFi/blob/master/README-ja.md) です。フルのプログラミング言語が使える組版システムであるところの SATySFi であれば、導出木をわかりやすく記述するためのDSLを作れそうです。実際にそれらしいものができたので、この記事で紹介します。

**注:** SATySFiの標準ライブラリは [`Proof` モジュール](https://github.com/gfngfn/SATySFi/blob/master/lib-satysfi/dist/packages/proof.satyh)を提供していてそちらでも導出木を書くことができます。`Proof`との比較は今は割愛します。

# インストール
今回の成果物は [satysfi-lib](https://github.com/nyuichi/satysfi-lib) におかせてもらっています。同じディレクトリに satysfi-lib をクローンした場合なら、以下のような import を書くだけで準備完了です。

```
@import: satysfi-lib/typeset/derive

% enjoy derive!
```

# 使い方

この import によって二つのモジュールが使えるようになります。

* `Derive` :  導出木を書くための数式コマンド `\proven` のみを提供
* `DeriveDsl` : `\proven` 中で導出木を構築するためのDSLを提供

モジュールを二つに分けているのは、`DeriveDsl` が衝突しやすそうな名前を多用しているためです。以下のような感じでDeriveはさっさと open する一方で、DeriveDSLは `\proven` 内の必要な部分だけで open するのが無難です。

```
@import: satysfi-lib/typeset/derive

open Derive in
% ....
  +math (${
    \proven!(
        open DeriveDSL in
        % Write DSL here
    )
  });
% ....
```

## `Derive` モジュール
### `\proven` : `[derivation-ast] math-command`
`\proven` コマンドは導出木を表示するための数式コマンドです。導出木を表すデータ `derivation-ast` を受け取ってレンダリングします。

```
${
    \proven!(
        % Write DSL here
    )
}
```

`!(...)`は数式モードからプログラムに切り替える構文で、この中でDSLを書いて `derivation-ast` のデータを構築します。

## `DeriveDsl` モジュール
`DeriveDsl` モジュールは `derivation-ast` を構築するための複数の関数から成ります。

### `derive` : `math -> derivation-ast`
`derive` は導出木を構築する上で最も基本的な関数です。数式を一つうけとって1.前件がなく 2.ラベルもなく 3.区切り線が普通の線の 導出木をつくります。

    open DeriveDSL in
    derive ${A \vdash A}

上のコードが以下のようにレンダリングされます。
![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/ffb18885-d1ed-21ea-b67b-80b1018b8e50.png)

`derive` の亜種で `assume` があります。これは基本的には `derive` と同じですが、導出の線が表示されません。

    open DeriveDSL in
    assume ${\vdash A}

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/f4e3f961-6ae2-27f6-0ca0-e471ca58b6c8.png)




### `by` : `inline-text -> derivation-ast -> derivation-ast`
`by` は導出にラベルを加える関数です。ラベルはinline-textで与えます。

    open DeriveDSL in
    by {Refl} (derive ${ A \vdash A })

上のように書くこともできますが、以下のようにパイプライン演算子を使うとコードがぐっと綺麗になります。

    open DeriveDSL in
    derive ${ A \vdash A }
    |> by {Refl}

どちらにせよ以下のようにレンダリングされます。

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/e92eedb7-eedf-6998-319c-e83abd1d9143.png)

同様の関数に`byOp`があります。ラベルはデフォルトで左側に表示されますが、`byOp`は反対側にラベルを表示します。

    open DeriveDSL in
    derive ${ A \vdash A }
    |> by {Refl}
    |> byOp {(1)}

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/d84889ca-4a2d-2605-684e-3bbe885f1520.png)


### `from` : `derivation-ast list -> derivation-ast -> derivation-ast`
`from` は導出に前提を追加する関数です。`from dlist d` で 「`dlist` の各導出から `d` を導く導出」を構築します。

    open DeriveDSL in
    derive ${ \vdash A \wedge B }
    |> by {${\wedge} I}
    |> from [
      assume ${\vdash A};
      assume ${\vdash B}
    ]

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/ea075e69-8302-966b-66ac-0e5562b9d2b0.png)

### `withLine` : `derivation-line -> derivation-ast -> derivation-ast`
`withLine` は導出の線を変更するための関数です。

今のところ `derivation-line` の値を作る方法は以下の3つです。

* `standard-line` : `derivation-line`
  - 直線  
* `no-line` : `derivation-line`
  - 線なし
* `dotted-line` : `length -> length -> derivation-line`
  - `dotted-line a b` で「黒線がa、空白がbが繰替えされる点線」を表す

`standard-line` と `no-line` は `derive` と `assume` で代用できるので実質的には `dotted-line` のための関数かもしれません。(あるいは「線はいらないけど`assume`って感じではないんだよなあ」という時にも使えます)

```
open DeriveDSL in
derive ${ \Gamma \vdash \Delta }
|> by {Cut}
|> withLine (dotted-line 2pt 1pt)
|> from [
  assume ${\Gamma \vdash \Delta, A};
  assume ${\Gamma, A \vdash \Delta}
]
```

![image.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/11817/cd6d65e6-a61d-02ad-a30e-ab6949abde75.png)

# 応用編 : デフォルトの設定を変える
実は `\Derive.proven` は一つオプショナル引数をとります。

    val \proven : [derive-config?; derivation-ast] math-cmd

この `derive-config` を明示的に渡すことでデフォルトの様々な設定を変えることができます。

* `by` によるラベルが右に置かれるか左に置かれるか
* `derive` で表示されるデフォルトの線
* その他導出木のレンダリングの細かい設定

まだこのあたりの設計は煮詰まっていないのでまた後日記事を書きます……

# まとめ
[satysfi-lib](https://github.com/nyuichi/satysfi-lib) を使うといい感じに導出木を書けるよ。