問題タブ [curry-howard]

論理プログラミングの基礎と、型システムと従来の論理との構文的類似性の現象との基本的な関係について教えてください。

私はプログラミングの人生の比較的遅い時期にカリーハワード同形性に出くわしました、そしておそらくこれは私がそれに完全に魅了されることに貢献しています。これは、すべてのプログラミングコンセプトに対して、形式論理に正確な類似物が存在すること、およびその逆が存在することを意味します。これが私の頭のてっぺんからのそのようなアナロジーの「基本的な」リストです：

それで、私の質問に：この同型写像のより興味深い/あいまいな意味のいくつかは何ですか？私は論理学者ではないので、このリストで表面をかじっただけだと確信しています。

たとえば、これは私が論理の中で下品な名前に気付いていないいくつかのプログラミングの概念です：

そして、ここに私がプログラミング用語で完全に特定していないいくつかの論理的な概念があります：

編集：

回答から収集されたいくつかの同等物は次のとおりです。

インターネットで調べてみたところ、論理理論の講義にどんどん退化していないCHIの説明が頭に浮かびました。（これらの人々は、「直感的な命題論理」が実際に普通の人間にとって何かを意味するフレーズであるかのように話します！）

大まかに言えば、CHIは、タイプは定理であり、プログラムはそれらの定理の証明であると言います。しかし、それは一体何を意味するのでしょうか？

これまでのところ、私はこれを理解しました：

• 考えてみてくださいid :: x -> x。そのタイプは、「Xが真であるとすると、Xが真であると結論付けることができます」と言います。私には合理的な定理のように思えます。

• ここで考えてみましょうfoo :: x -> y。Haskellプログラマーなら誰でも言うように、これは不可能です。この関数を書くことはできません。（まあ、とにかく騙さずに。）定理として読むと、「Xが真であるとすれば、Yは真であると結論付けることができます」と書かれています。これは明らかにナンセンスです。そして、確かに、この関数を書くことはできません。

• より一般的には、関数の引数は「これが真であると見なされる」と見なすことができ、結果タイプは「他のすべてが真であると仮定して真である」と見なすことができます。たとえば、関数の引数がx -> yある場合、Xが真であるということは、Yが真でなければならないことを意味すると仮定することができます。

• たとえば、(.) :: (y -> z) -> (x -> y) -> x -> z「YがZを含意し、XがYを含意し、Xが真であると仮定すると、Zが真であると結論付けることができます」と見なすことができます。これは私には論理的に理にかなっているようです。

さて、一体どういうInt -> Int意味ですか？o_O

私が思いつくことができる唯一の賢明な答えはこれです：関数X-> Y-> Zがある場合、型シグネチャは「タイプXの値とタイプYの値を作成できると仮定すると、タイプZ"の値を作成することができます。そして、関数本体は、これをどのように行うかを正確に記述します。

それは理にかなっているようですが、あまり面白くありません。だから明らかにこれ以上のものがあるに違いない...

そこで、より高度な Haskell/GHC の機能と概念のいくつかを理解できるようにするために、動的に型指定されたデータの実用的な GADT ベースの実装を取り上げ、それを拡張してパラメトリック型をカバーすることにしました。(この例が長くなって申し訳ありません。)

ただし、これのコンパイルは最後の行で失敗します (私の行番号は例と一致しません):

私がこれを読んだ方法では、コンパイラは でそれを理解できず、Inductive :: Equal a b -> Equal (f a) (f b)底以外の値と等しくなければなりませんa。bだから私は試しましたがInductive :: Equal a a -> Equal (f a) (f a)、それも失敗し、の定義でmatchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b):

matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b)生成するの型を変更してmatchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a a)も機能しません (命題として読んでください)。どちらもしませんmatchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal a a)(別の些細な命題です。私が理解しているように、これにはTypeRep a fromDynamic' to know theDynamic`のユーザーが必要です)。in thecontained in the

だから、私は困惑しています。ここで前進する方法についての指針はありますか？

Set、同様に[]完全に定義されたモナド操作を持っています。問題は、値が制約を満たす必要があるため、制約なしOrdで定義することは不可能です。同じ問題は、可能な値に対して何らかの制約を必要とする他の多くのデータ構造にも当てはまります。return>>=

標準的なトリック ( haskell-cafe の投稿Setで私に提案された) は、継続モナドにラップすることです。ContT基になる型ファンクターに制約があるかどうかは気にしません。制約は、Sets を継続に/からラップ/アンラップする場合にのみ必要になります。

これは必要に応じて機能します。たとえば、引数を 1 増やすか、そのままにしておく非決定論的関数をシミュレートできます。

確かに、stepN 5 0利回りfromList [0,1,2,3,4,5]. []代わりにモナドを使用すると、次のようになります

代わりは。

問題は効率です。を呼び出すとstepN 20 0、出力に数秒かかり、stepN 30 0妥当な時間内に終了しません。Set.union各モナド計算の後に実行するのではなく、すべての操作が最後に実行されることがわかります。その結果、指数関数的に多くSetの が構築さunionれ、最後にのみ編集されることになり、これはほとんどのタスクでは受け入れられません。

この構造を効率的にするために、それを回避する方法はありますか? 私は試しましたが、成功しませんでした。

(私は、カリー・ハワード同型とグリベンコの定理から、ある種の理論的限界があるのではないかとさえ思っています。グリベンコの定理は、任意の命題トートロジーφに対して、式¬¬φは直観論的論理で証明できると述べています。しかし、私は、証明の長さは (通常の形式で) 指数関数的に長くなる可能性があります. したがって, 計算を継続モナドにラップすると指数関数的に長くなる場合があるかもしれません?)

Curry-Howard 同形により、 ScalaUnitは論理 true とNothing論理 false に対応します。論理的 true が何によっても暗示されるという事実は、引数を破棄するだけの単純な関数によって証明されます。

論理 false が何かを意味するという事実を目撃する関数はありますか、それは type の関数Nothing => Aですか? または、それを構築する慣用的な方法はありますか?

いつでも次のようなことができます

しかし、これは醜いだけです-値がないという事実を使用していませんNothing。例外なくそれを行う方法があるはずです。

のabsurd関数にData.Voidは次のシグネチャがあります。ここで、Voidはそのパッケージによってエクスポートされた論理的に無人のタイプです。

私は、これがタイプとしての命題の対応によって、有効な式に対応するというドキュメントのコメントを取得するのに十分なロジックを知っています⊥ → a。

私が困惑して興味を持っているのは、この関数がどのような実用的なプログラミングの問題に役立つのかということです。「起こりえない」ケースを徹底的に処理するタイプセーフな方法として役立つ場合もあると思いますが、カリー・ハワードの実際の使用法については、そのアイデアがまったく正しいトラック。

編集：できればHaskellの例ですが、依存型の言語を使用したい場合は、文句を言うつもりはありません...

そのため、小さな Haskell の演習を通じて Curry-Howard を半分理解しようとする継続的な試みの中で、私はこの時点で行き詰まってしまいました。

明らかに、型Equal Int Charには (非底部の) 居住者がいないため、意味的には関数が存在するはずabsurdEquality :: Equal Int Char -> aです...しかし、私の人生では、を使用する以外に書く方法がわかりませんundefined。

したがって、次のいずれかです。

1. 何かが足りない、または
2. これを不可能な作業にする言語のいくつかの制限があり、それが何であるかを理解することができませんでした.

答えは次のようなものだと思います。コンパイラはEqual、a = b を持たないコンストラクターがないという事実を利用できません。しかし、もしそうなら、何がそれを真実にするのでしょうか?

私はこれを何時間も理解できずに見つめていました:(

coq を使用していくつかの定義を解決する必要があり、Curry Howard 同型を介して解決することになっています。私は読んだことがありますが、自分が何をしているのかまだわかりません。私は他の例を見て、そのようにしてみましたが、常にエラーが発生します。

たとえば、ここでは次のように定義する必要があります。

これは私の試みでした：

私も試しました

最終的には、私が与えたものとは異なるタイプを期待していたとだけで、「タイプが「?9 * ?10」であると予想される」などのように表示されることもあります。

私が見つけたすべてを読んだ後、これを理解するのに本当に苦労しています。

誰か説明してください:(

「Löb と möb: Haskell の奇妙なループ」を理解しようとしていますが、今のところその意味は私から離れています。なぜそれが役立つのかわかりません。Just to Recall 関数loebは次のように定義されます。

または同等：

この記事には、[]ファンクターとスプレッドシートの実装の例がありますが、スプレッドシート自体と同じように、私にとっては少し異質です（使用したことはありません）。

私はそのスプレッドシートのことを理解していますが、リストに関係なく、私や他の人にとってより多くの例があると非常に役立つと思います. loebforMaybeまたは他のファンクターのアプリケーションはありますか?