保証〈warranty〉 ： derivation T → A 反駁〈refutation〉 ： derivation A → ⊥ 証拠〈witness〉 ： 存在記号導入に使う要素、項 事例〈instance〉 ： 全称記号消去に使う要素、項 存在スタート条件〈existential starting condition〉 ： 存在記号消去に伴…

data Tree a = Leaf a | Tree (Tree a) (Tree a) 値コンストラクタ、型コンストラクタ、型が紛らわしいという例。値コンストラクタをタグだと考えると： type Tree<A> = @Leaf A | @Tree [Tree<A>, Tree<A>] タグ @Leaf, @Tree に対応する値コンストラクタを ^Leaf, ^</a></a></a>…

対象物： 型 関数 値〈データ | ポイント〉 特別な関数 汎関数〈メタ関数〉 命題（真偽値、述語、論理式） 導出 保証 特別な導出 リーズニング〈メタ導出〉 カリー／ハワード／ランベック対応 型 命題 関数 導出 値 保証 汎関数 リーズニング 項： 型項（多…

https://arxiv.org/abs/2102.03044 から。 証明が行うこと 読者の心に形成されるもの guarantee trust explain insight, understanding

https://arxiv.org/abs/2102.03044 の冒頭、同語義： {mathematical | logical | rigorous | formal | rational}* {derivation | proof} 単なる多義語ならいいのだけど、実際には曖昧語になっているのがタチが悪い。

動詞 DoSomething 名詞 Something 短縮 construct construction cons calculate calculation calc derive derivation deriv reason reasoning reas Begin Something WeHave A And, B Using Something X params WeHave A' And, B' Using Something Y params .…