次のようなキーワードの名前スコープと使い方について考える。
- def, theorem
- let in, let return
- providing return where
- section
- module
- package
名前とスコープに関する概念：
- イミュータブル名〈プログラム定数〉とミュータブル名〈プログラム変数〉
- 公理定数
- シャドーイング
- オーバーライト〈アップデート〉
- 名前のオーバーロード
スクリプトの文は次がある。
- 命令文〈command sentence〉 例： toward p doPostCompose f
- 記述文〈descriptive sentence〉
命令文で状態遷移が起こり、ムービーのフレームが進む。フレーム内のステージとシーケントが変化する。一方、記述文は、フレーム／ステージ／シーケントの状況を記述する。記述文では何も起こらない。
命題ではなくて、常に証明〈計算手順〉とシーケントを見る。操作対象は証明。命題は証明の域・余域なだけ。
命令文の例：
- getFact シーケント
- toward 判断シーケント addToContext 宣言
- toward 質問シーケント removeFromContext 宣言
- toward 質問質問 hit 事実シーケント
- create stage ‥‥
- close stage
- {assert | show{ed}? | proved} 命題 from 証明
- return 計算 of 型
記述文の例：
- we {gained | obtained} 命題 from 証明
- we reached 型 from 計算
- we have {命題 | 型} from {証明 | 計算}
ステージの操作：
create stage ariving at P∧Q∧R factor 1 ‥‥ factor 2 ‥‥ factor 3 ‥‥ close stage we obtained p: |- P∧Q∧R create stage departing fromt P∨Q∨R case 1 ‥‥ case 2 ‥‥ case 3 ‥‥ close stage we obtained q: P∨Q∨R |- S create stage ariving at ∀(x:X).P(x) x:X ‥‥ we showed P(x) close state we gained p: |- ∀(x:X).P(x) create stage departing from ∃(x:X).P(x) x:X ‥‥ we showed Q close stage we gained p: ∃(x:X).P(x) |- Q
その他、キーワード候補
- we reached Y via f ≡ we showed Y from f ≡ return f of Y
- we showed Y from f ≡ we showed Y because of f
- providing ‥‥ we proved Y because of f where ‥‥
- showing T suffices to show Y because of f
- we attempt to show T
