計算可能な関数のプログラミング

コンピュータサイエンスにおいて、プログラミング計算可能関数（PCF）、またはプログラミング計算可能関数、またはプログラミング計算可能関数用言語は、 1977年にゴードン・プロトキンによって導入された型付き関数型プログラミングに基づくプログラミング言語であり、ダナ・スコットによる以前の^未発表資料に基づいている。^{[ 1 ]これは、}型付きラムダ計算の拡張版、またはMLやHaskellなどの現代^の型付き関数型言語の簡略版と考えることができる。

PCF の完全抽象モデルは、最初に Robin Milner によって提示されました。[ 2 ]^{しかし、Milner}のモデルは基本的に PCF の構文に基づいていたため、満足のいくものではないと考えられていました。^{[ 3 ]}構文を使用しない最初の 2 つの完全抽象モデルは、1990 年代に定式化されました。これらのモデルは、ゲーム意味論^{[ 4 ] [ 5 ]}と Kripke 論理関係に基づいています。^{[ 6 ]}しばらくの間、これらのモデルはどちらも効果的に表現できないため、完全に満足のいくものではないと考えられていました。しかし、Ralph Loader は、PCF の有限断片におけるプログラム等価性の問題が決定できないため、効果的に表現できる完全抽象モデルは存在し得ないことを示しました。^{[ 7 ]}

PCFのデータ型は帰納的に次のように定義される。

• natは型です
• 型σとτに対して、関数型σ → τが存在する。

コンテキストとは、変数名 x と型 σのペアのリストであり、変数名が重複しないようにします。次に、以下の構文構造に対して、通常の方法でコンテキスト内の項の型判定を定義します。

• 変数 ( x  : σがコンテキストΓの一部である場合、Γ ⊢ x  : σ )
• （ σ → τ型の項をσ型の項に適用する）
• λ抽象化
• Y固定点コンビネータ（型σから型σの項を作成する）→ σ
• natと定数0に対する後継 ( succ ) および前任 ( pred ) 操作
• 型付けルール付きの条件式if ：

${\displaystyle {\frac {\Gamma \;\vdash \;t\;:{\textbf {nat}},\quad \quad \Gamma \;\vdash \;s_{0}\;:\sigma ,\quad \quad \Gamma \;\vdash \;s_{1}\;:\sigma }{\Gamma \;\vdash \;{\textbf {if}}(t,s_{0},s_{1})\;:\シグマ }}}$

（ここでは、 nat s はブール値として解釈され、ゼロは真、その他の数値は偽を表すという慣例に従います。）

• Scott, Dana S. (1969). "CUCH、ISWIM、OWHYに対する型理論的な代替案" (PDF) .未発表原稿.Scott, Dana S. (1993). "A type-theoretic alternative to CUCH, ISWIM, OWHY" . Theoretical Computer Science . 121 : 411–440 . doi : 10.1016/0304-3975(93)90095-b .として発表。
• ミッチェル、ジョン・C. (1996). 「言語PCF」 .プログラミング言語の基礎. MIT Press. ISBN 9780262133210。

• RealPCF入門
• PCF用の字句解析器と構文解析器はSMLで記述されている。