ルディックス

証明理論において、ルーディクスは数学的論理の推論規則を支配する原理の分析である。ルーディクスの主な特徴には、複合接続詞の概念、フォーカシングまたはフォーカライゼーション（コンピューター科学者のジャン＝マルク・アンドレオリが発明）として知られる手法の使用、命題の代わりに基底上の位置または軌跡の使用などがある。

より正確に言えば、ルディックスは、密接に関連するゲームセマンティクスで行われているのと同様に、インタラクティブコンピューティングのパラダイムに従って、既知の論理接続詞と証明動作を取得しようとします。数式の概念を抽象化し、その具体的な使用法、つまり個別の発生に焦点を当てることで、場所をメモリ上の ポインターと見なすことができるため、コンピューターサイエンスの抽象構文を提供します。

ルーディクスの主な成果は、2 つの自然ではあるが異なる型または命題 の概念間の関係を発見したことです。

最初の見解は、命題の証明理論的解釈またはゲンツェンスタイルの解釈とも呼ばれ、命題の意味はその導入規則と除去規則から生じるというものです。焦点化は、意味が導入規則から生じる肯定命題と、意味が除去規則から生じる否定命題を区別することで、この見解を洗練させます。焦点化計算では、導入規則のみを与えることで肯定接続詞を定義することができ、除去規則の形状はこの選択によって強制されます。(対照的に、否定接続詞は焦点化計算で除去規則のみを与えることで定義でき、導入規則はこの選択によって強制されます。)

2 番目の見解は、命題の計算的解釈またはBrouwer-Heyting-Kolmogorov 解釈とも呼ばれ、計算システムを事前に固定し、次に命題の実現可能性解釈を与えて、命題に構成的な内容を与えるという見解をとっています。たとえば、「A は B を意味する」という命題の実現子は、A の実現子を受け取り、それを使用して B の実現子を計算する計算可能な関数です。実現可能性モデルは、命題の実現子を、その内部構造ではなく、目に見える動作の観点から特徴付けます。

ジラールは、 2 次 アフィン 線形論理の場合、非停止性とエラー停止を効果とする計算システムが与えられたとき、実現可能性と焦点化が型に同じ意味を与える ことを示しています。

ルーディクスは論理学者 ジャン＝イヴ・ジラールによって提唱された。ルーディクスを紹介した彼の論文「Locus solum: 論理の規則から規則の論理へ」には、数理論理学の出版物としては風変わりと思われる特徴がいくつかある（スカンクの図解など）。これらの特徴の意図は、執筆当時のジャン＝イヴ・ジラールの視点を強化することにある。そして、それによって読者に、背景に関係なくルーディクスを理解する可能性を提供している。 ^{[疑わしい–議論が必要] [引用が必要]}

1. Girard, J.-Y.、「Locus solum: 論理のルールからルールのロジックへ」(.pdf)、「コンピュータサイエンスにおける数学的構造」、11、301–506、2001 年。
2. カーネギーメロン大学のジラード読書会（Locus Solum に関するウィキ）