haskell - C で自然数を加算できないことの結果

Question

システム FI では、教会数を使用して真の全加算関数を定義できます。

Haskell では、下の値のためにその関数を定義できません。たとえば、haskell では、x + y = x の場合、y がゼロであるとは言えません。x が底の場合、任意の y について x + y = x です。したがって、足し算は真の足し算ではなく、その近似値です。

C仕様では、すべてに有限サイズが必要であるため、CIではその関数を定義できません。そのため、C では可能な近似は Haskell よりもさらに悪いものになります。

したがって、次のようになります。

System F では、加算を定義することはできますが、完全な実装を行うことはできません (無限のハードウェアがないため)。

Haskell では、追加を定義することはできず (底のため)、完全な実装を持つことはできません。

C では、合計加算関数を定義することはできません (すべてのセマンティックが制限されているため) が、準拠した実装は可能です。

したがって、3 つの正式なシステム (Haskell、システム F、および C) はすべて、設計上のトレードオフが異なるようです。

では、どちらか一方を選択すると、どのような結果が生じるでしょうか。

Answer 1

Answer 2

推論を行うためのフレームワークとして一連の理論があります。有限現実、Haskell セマンティクス、システム F はその 1 つにすぎません。

作業に適した理論を選択し、ゼロから新しい理論を構築することも、既存の理論の大きな断片を集めて構築することもできます。たとえば、Haskell プログラムを常に終了させるセットを検討し、底なしのセマンティクスを安全に使用できます。この場合、あなたの追加は正しいでしょう。

低レベルの言語では、有限性をプラグインする考慮事項があるかもしれませんが、高レベルの言語では、より抽象的な理論がより広い適用を可能にするため、そのようなことを省略する価値があります。

プログラミングでは「言語仕様」理論ではなく「言語仕様＋実装制限」理論を使うので、言語仕様にメモリ制限がある場合と言語実装にメモリ制限がある場合とで違いはありません。言語セマンティクスのフレームワークで純粋な理論的構造を構築し始めると、制限がないことが重要になります。たとえば、プログラムの同等性や言語の翻訳を証明したい場合、言語仕様に不要な詳細があると、証明に苦労することがあります。

Answer 3

「理論的には理論と実践の間に違いはないが、実際には違いがある」という格言を聞いたことがあると思います。

この場合、理論的には違いがありますが、これらのシステムはすべて同じ有限量のアドレス可能なメモリを処理するため、実際には違いはありません。

編集：

これらのシステムのいずれかで自然数を表すことができると仮定すると、それらのいずれかで加算を表すことができます。懸念している制約により自然数を表現できない場合は、Nat*Nat加算を表現できません。

自然数を（最大ビットサイズのヒューリスティックな下限と遅延評価されたビットのリスト）のペアとして表します。

ラムダ計算では、trueで呼び出された関数が1のビットを返し、falseで呼び出された関数が2のビットに対して同じことを行う関数を返す関数として、リストを表すことができます。

加算は、キャリービットを伝播する2つのレイジーリストのzipに適用される操作です。

もちろん、最大ビットサイズのヒューリスティックを自然数として表す必要がありますが、表現している数値よりも厳密に小さいビット数の数値のみをインスタンス化し、演算子がそのヒューリスティックを破らない場合は、ビットサイズは、操作したい数値よりも誘導的に小さい問題であるため、操作は終了します。

エッジケースの説明を簡単にするために、Cはほとんど役に立ちません。オーバーフロー/アンダーフローを表す特別な値を返すことができ、それらを感染性にすることもできます（IEEE-754 NaNなど）が、チェックに失敗した場合、コンパイル時に苦情を受け取ることはありません。シグナルSIGFPEまたはトラップの問題に類似したものをオーバーロードしてみてください。

yがゼロであるとは言えません。xが下の場合、任意のyに対してx + y=xです。

記号操作を行う場合、MatlabとMathematicaはCおよびCのような言語で実装されています。とは言うものの、Pythonには、すべての整数型に使用される、十分に最適化されたbigint実装があります。ただし、実際に非常に大きな数を表すにはおそらく適していません。