2

https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Implication/level/0

上記のLeanを用いたNatural Number GameのWorld: Implication Worldを解いてると、型で証明できそうな気はしてきたのですが、カリー=ハワード同型対応 (Wikipedia) には以下のような記述がありました。

論理 プログラミング
真 ⊤ トップ型 1
偽 ⊥ ボトム型 0

いままで、素朴なプログラミング言語では true, false はブーリアン型という認識だったのですが、急にトップ型とボトム型が登場しました。論理(数学)の真偽とプログラミングのtrue, falseは別物なのでしょうか? いままで同じようなものだと思い、それがブーリアン型だと思っていたのですが... なにか文脈が違うのでしょうか? それとも boolean = トップ型 1 | ボトム型 0 みたいなことでしょうか?


追記:
https://proofassistants.stackexchange.com/questions/4185/the-relationship-between-true-formula-and-types-in-the-curry-howard-correspond にも質問しました(やり取り中ですが、私の数学力が低くて承認できなさそうです)。質問の過程で英語版のWikipediaの内容が変わりました(回答者が英語版Wikipediaを編集しました。そもそも日本語版と英語版で異なっていましたが、大幅に書きかわりました)。

2
  • 「本家(英語Wiki)」では異なる説明のようです。
    – Uncle-Kei
    Commented 7月16日 9:08
  • @Uncle-Kei 失礼しました。姉妹サイトに質問し、その過程で書きかわりました(そもそも日本語版と英語版で異なっていましたが、大幅に書きかわりました)。質問に追記しておきました。 Commented 7月16日 10:06

1 件の回答 1

1

左の世界での真は、命題が証明されていること、もしくは、証明された命題の意味です。
左の世界での偽は、命題の否定が証明されていること、もしくは、否定が証明された命題の意味です。
(命題Pがあって、Pが証明可能なら真、¬Pが証明可能なら偽)

左の世界で真や偽と言ったら、それは命題のことです。
左の世界の命題は右の世界のに対応するので、表の右側に出てくるのはでなければなりません。
ブーリアン型のであるtrueやfalse、数値型のである1や0が表の右側に登場するのはおかしいです。

左の世界「証明する」が、右の世界の「インスタンスが存在する」に対応するので、左の世界の真に対応する右の世界の型が、unit type でなければならないという理由はありません。文字列型でも整数型でも、それこそboolean型でも(インスタンスが存在すると保証されているので)よいです。
ただ、「唯一のインスタンスを持つ」という性質が名前になっているから unit type だとわかりやすい、というだけのことかと思います。

左の世界での偽に対応する、右の世界の性質は「インスタンスが作れないと保証されている」になります。

追記: 迂闊に、オブジェクト指向っぽく「インスタンスが作れる」と書いちゃいましたがラムダ計算との対応としては「式が作れる」の方がよいですね。

7
  • > 「式が作れる」. 英語だと「A type is said to be inhabited if it has some elements.」とされており、おそらくelementが、おっしゃている「式」のことかと推測するしています。またinhabitedに関しては、aconite-ac.github.io/theorem_proving_in_lean4_ja/… にも記載がるのですが > inhabited(有項) と呼び、型 p が持つ項 * をinhabitant(住人) と呼ぶ。 なにかご存知だったりしませんでしょうか?独特の言い回しが多く、理解できておりません。(なお、unit typeに関しては、姉妹サイトに質問した後で、とにかく1つでもあればなんでもよさそうと私も感じておりますので、同意見です) Commented 7月21日 0:40
  • 例えば TypeScriptのNever型、例えばScalaのNothing型、これらはその型のオブジェクトを作ることができません。そのような性質を持った型はBottom Typeと呼ばれます。ScalaのNothing型はほかのすべての型のサブクラスとして振る舞うからです。また、だからこそインスタンスの生成ができません(インスタンスがあると型システムが矛盾するので)。型がインスタンス/オブジェクト/式/項/element を持つことを inhabite と言うし、インスタンス/オブジェクト/式/項/element を持つ型をinhabited(有項) と呼ぶ、それだけではないでしょうか?
    – quickquip
    Commented 7月21日 2:58
  • up voteしました。おっしゃるとおりな気がします。ただ、現段階で正確に正しいのか私に判断することができず、承認はできなさそうです。(少なくとも私が普段使っているプログラミング言語では見かけない用語が多いです。特に、項やinhabitedやelement)/ ちなみに、ボトム型は「式が作れない」という言い方になるという認識であっていますでしょうか? Commented 7月21日 3:17
  • ボトム型は「ほかのすべての型のサブクラスであるような型」が 定義 で、型システムの要件上「インスタンス/オブジェクト/式が作れない」という 性質 を持ちます。英語版Wikipediaで書き直された Never type は「インスタンス/オブジェクト/式が作れない」が 定義 です。 TypeScriptならNever型、ScalaならNothing型、PythonのTypingモジュールではNeverやNoReturnとしてでてきます(Pythonはただの型チェック用なのでものは違うかもしれませんが)。用語が違いますが、それらを総称するとしたらどうしますか? オブジェクト指向言語なら「インスタンスが作れる」、関数型言語なら「式が作れる」で用語が違いますね???? それらを総称するならどうしますか??? また、それらに共通する概念を持ってないから語として総称が登場してもピンとこない、という話ですか?
    – quickquip
    Commented 7月21日 3:27
  • 抽象度が一段上がっている時に、具象の(個別の既知のプログラミング言語の)用語に引っ張られないように、別の語を用意するのはわりと納得がいく話だと思いますが……
    – quickquip
    Commented 7月21日 3:32

この質問に回答するには、ログインする必要があります。

求めていた回答ではありませんか? のタグが付いた他の質問を参照する。