globular風の自然演繹系
自然演繹系のUIをglobular風にする。
| globular | 自然演繹系 |
|---|---|
| パレット | パレット |
| セル | 項（ターム） |
| ラベル | ラベル（名前） |
| 色 | (なし) |
| 次元 | 次元 |
| ダイアグラム | 式 |
| キャンバス | ノート |
| キャンバスビュー | ノートエリア |
| コマンド | コマンド |
コマンド
Globularのコマンドは少なくて（Globularの使い方 (2)： サンプル・ワークスペース - 檜山正幸のキマイラ飼育記参照）：
- New
- Make
- Source, Target
- Select
- Attach
- Theorem
自然演繹風だと次のようになるだろう。
特殊なコマンド
- New 何もない所から新しい0項を作り、パレットに入れる。*⇒0
- Del パレットから項を削除する。n⇒* 依存する項もすべて消す。
- Axiom 命題を公理として設定する。0⇒1
- Def 式に名前を付けてパレットに入れる。n⇒n+1
ノート上で使うコマンド
- conj, disj, impl : 0, 0⇒0
- neg : 0⇒0
- id : 0⇒1
- proj1, proj2 : 0, 0⇒1
- inj1, inj2 : 0, 0⇒1
- eval : 0, 0⇒0
- confl : 0, 0⇒0
- curry : 1⇒1
- pair : 1, 1⇒1
- copair : 1, 1⇒1
- comp: 1, 1⇒1
コマンドの発火条件
コマンドが発火するには、引数（オペランド）が特定のパターンを持っている必要があるんで、パターンマッチングでチェックして、発火条件が満たされたときだけ実行される。
例：
- eval : A, A⊃B ⇒ B
Undo
トップレベルコマンドは、Do(コマンド), Undo, Redo。これらはログツリーを成長させていく。
- Do(コマンド) ：現在のノード（状態のーど）の最後の子として、コマンドの実行結果を追加する。コマンド自体もログツリーに記録する。
- Undo : 現在のノードの親のノードに移り、状態も親と同じにする。
- Redo ： 現在のノードの最後の子のノードに移り、状態も子と同じにする。
ログツリーを直接にナビゲートするには、
- parent, firstChild, lastChild, prevSibling, nextSibling, oldestSibling, eldestSiblingを使う。
- コマンドと状態には、発行順に通し番号が付けられるので、その番号でも移動可能。
- ログツリーとは別にヒストリーリストにも記録される。
