mandel59 https://blog.hatena.ne.jp/mandel59/ Ryusei’s Notes (a.k.a. M59のブログ) https://mandel59.hateblo.jp/ プログラミング 表明から証明へ (2) 型と命題 カリー゠ハワード同型対応により、プログラムと証明が対応すると述べた。実際にはどのように対応しているのだろうか? 実は、恒真である命題は、空でない（その型である値を持つ）型に対応しているのだ。 型と命題の対応関係を見てみよう。 型 命題 (x : A) -> P x (x : A ** P x) Not P (P, Q) Either P Q P -> Q ここで、NotはBuiltins.idrで次のように定義されている。 Not : Type -> Type Not a = a -> _|__|_ という奇妙な型は、HaskellのData.Void型と同じ… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmandel59.hateblo.jp%2Fentry%2F2013%2F09%2F14%2F115924" title="こわくない Idris (5) - Ryusei’s Notes (a.k.a. M59のブログ)" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> http://chart.apis.google.com/chart?cht=tx&chl=%5Cforall%20x%20%5Cin%20A%20%28P%28x%29%29 Hatena Blog https://hatena.blog 2013-09-14 11:59:24 rich https://mandel59.hateblo.jp/entry/2013/09/14/115924 1.0 100%