oop - 関数型プログラミングはより「数学的」と見なされますか? もしそうなら、なぜですか？

Question

ときどき、「関数型プログラミング言語の方が数学的だ」などと言う人を耳にします。そうですか？もしそうなら、なぜ、どのように？たとえば、Scheme は Java や C よりも数学的ですか? それともハスケル？

「数学的」とは何かを正確に定義することはできませんが、感覚はつかめると思います。

ありがとう！

Answer 1

2 つの一般的な (*)計算モデルがあります:ラムダ計算(LC) モデルとチューリング マシン(TM) モデルです。

ラムダ計算は、型のドメイン上の関数の構成によって結果が生成される数学的形式を使用して計算を表現することにより、計算にアプローチします。LC は、同じトピックに対するより一般化されたアプローチと見なされるCombinatory Logicにも関連しています。

チューリング マシンモデルは、基本的な操作 (加算、突然変異など) の本体を使用して、理想化されたストレージに格納されたシンボルの操作として計算を表現することで、計算にアプローチします。

これらのさまざまな計算モデルは、プログラミング言語のさまざまなファミリーの基礎となっています。ラムダ計算は、 ML、Scheme、Haskellなどの言語を生み出しました。チューリング モデルはC、C++、Pascalなどを生み出しました。一般化として、ほとんどの関数型プログラミング言語は、ラムダ計算に理論的基盤を持っています。

ラムダ計算の性質上、その原理に基づいて構築されたシステムの動作について特定の証明が可能です。実際、証明可能性 (つまり、正しさ) は LC の重要な概念であり、LC システムに関する特定の種類の推論と結論を可能にします。LC は型理論と圏論にも関連しています (そして依存しています)。

対照的に、チューリング モデルは型理論にあまり依存せず、基礎となるモデルの一連の状態遷移として計算を構造化することに依存します。チューリング マシンの計算モデルは、アサーションを行うのがより難しく、LC ベースのプログラムが行うのと同じ種類の数学的証明や操作には向いていません。ただし、これはそのような分析が不可能であることを意味するものではありません。TM モデルのいくつかの重要な側面は、プログラムの仮想化と静的分析を研究するときに使用されます。

関数型プログラミングは型の慎重な選択と型間の変換に依存しているため、FP はより「数学的」と見なすことができます。

(*) 他の計算モデルも存在しますが、この議論にはあまり関係ありません。

Answer 2

純粋な関数型プログラミング言語は関数型計算の例であるため、理論的には関数型言語で記述されたプログラムは数学的な意味で推論できます。理想的には、プログラムが正しいことを「証明」できるようにしたいと考えています。

実際には、そのような推論は些細な場合を除いて非常に困難ですが、それでもある程度は可能です。プログラムの特定のプロパティを証明できる場合があります。たとえば、プログラムへのすべての数値入力が与えられた場合、出力は常に特定の範囲内に制限されることを証明できる場合があります。

ミュータブルな状態と副作用を伴う非関数型言語では、プログラムについて推論し、正確性を「証明」しようとする試みは、少なくとも現時点ではほとんど不可能です。機能しないプログラムでは、プログラムを熟考してその一部が正しいことを確信でき、特定の入力をテストする単体テストを実行できますが、通常、プログラムの動作に関する厳密な数学的証明を構築することはできません。

Answer 3

主な理由の 1 つは、純粋な関数型言語には副作用がないことです。つまり、変更可能な状態がなく、入力パラメーターを結果値にマップするだけであり、これはまさに数学関数が行うことです。

Answer 4

関数型プログラミングの論理構造は、ラムダ計算に大きく基づいています。数学の代数形式だけに基づいた数学ではないように見えるかもしれませんが、離散数学から非常に簡単に記述できます。

命令型プログラミングと比較して、何かを行う方法を正確に規定するのではなく、何をしなければならないかを規定します。これはトポロジを反映しています。

Answer 5

関数型プログラミング言語の数学的感覚は、いくつかの異なる機能に由来します。最も明白なのは名前です。「関数型」、つまり数学の基本である関数を使用します。もう 1 つの重要な理由は、関数型プログラミングでは、常に真であるものの集合を定義する必要があり、それらの相互作用によって目的の計算が実現されるためです。これは、数学的な証明が行われる方法と似ています。