Free Bi-Cartesian Closed Category (BCCC) の決定問題は決定可能ですか? 同様に、単純型付けされたラムダ計算を強力な n 項積と和で拡張した場合、等式は決定可能ですか? 無料のほぼBCCC の決定問題は決定可能です。
http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf
しかし、この作業には初期オブジェクト、またはラムダ計算用語の空の型は含まれていませんが、彼らのメソッドは BCCC に拡張できると推測しています。
1 に答える
0
最初のオブジェクトが除外されている理由を説明するのに役立つ部分的な回答を提供します。初期オブジェクトが指数関数と組み合わされると、物事は崩壊し始めます。または共指数を持つ終端オブジェクト。この崩壊は、指数関数と共指数関数の両方が存在する場合に完全になります。その場合、決定可能性の問題は自明になり、ロジックの証明可能性に還元されますが、「通常の形式」の削減問題はより困難になります-皮肉なことに。
こちらに詳細を掲載しました。ここではお答えできません。StackOverflow の「不適切な形式のコード」の誤検出バグにより、インターフェイスが修復できないほど壊れているためです。(空の表示ウィンドウでもわかります。これはコンピューターの質問でさえないので、私の答えにはコンピュータープログラミングはありません!)
https://math.stackexchange.com/questions/4032422/decidability-of-bi-cartesian-closed-categories
于 2021-02-19T22:41:32.367 に答える