高階抽象構文

コンピュータサイエンスにおいて、高階抽象構文（HOASと略される）は、変数バインダーを持つ言語の抽象構文木を表現するための手法です。

抽象構文が抽象的である理由は、本質的に特定の構造を持つ数学的オブジェクトによって表現されるからです。たとえば、コンパイラで一般的に使用される第一階抽象構文( FOAS ) ツリーでは、ツリー構造によって部分式関係が暗黙的に示されます。つまり、プログラムの曖昧さを解消するために括弧は必要ありません (具象構文では括弧が使用されています)。HOAS は、変数とその結合サイトの関係という追加の構造を公開します。FOAS 表現では、変数は通常、識別子で表現され、結合サイトと使用の関係は同じ識別子を使用して示されます。HOAS では、変数の名前はありません。変数を使用するたびに、結合サイトが直接参照されます。

この手法が便利な理由はいくつかあります。まず、プログラムのバインディング構造が明確になります。FOAS 表現で演算子の優先順位を説明する必要がないのと同様に、HOAS 表現を解釈するためにバインディングとスコープのルールを把握する必要はありません。次に、 アルファ同等のプログラム(バインドされた変数の名前のみが異なる) は HOAS で同一の表現を持つため、同等性チェックがより効率的になります。

HOAS を実装するために使用できる数学的オブジェクトの 1 つは、変数がエッジを介して結合サイトに関連付けられているグラフです。HOAS を実装するもう 1 つの一般的な方法 (たとえば、コンパイラ内) は、de Bruijn インデックスを使用することです。

構文におけるλ束縛を直接サポートした最初のプログラミング言語は、高階論理プログラミング 言語λPrologでした。^[1] HOASという用語を導入した論文^[2] では、λPrologコードを使用してそれを説明しました。残念ながら、HOASという用語を論理プログラミングから関数型プログラミングの 設定に移すと、その用語は構文における束縛を式に対する関数と同一視することを意味します。この後者の設定では、HOASは異なる問題のある意味を持ちます。λ木構文という用語は、論理プログラミングの設定で使用可能な表現スタイルを具体的に参照するために導入されました。^{[3] [4]} 詳細は異なりますが、λPrologでの束縛の扱いは、次のセクションで詳しく説明する論理フレームワークでの扱いに似ています。

論理フレームワークの分野では、高階抽象構文という用語は通常、メタ言語のバインダーを使用してオブジェクト言語のバインディング構造をエンコードする特定の表現を指すために使用されます。

たとえば、論理フレームワークLF には、矢印 (→) 型の λ 構造があります。例として、型指定のない式、組み込みの変数セット、および式で定義を使用して変数をバインドできる let 構造 ( )をlet <var> = <exp> in <exp'>持つ非常に原始的な言語を形式化したいとします。Twelf 構文では、次のように実行できます。 varexpexp'

 exp : type.var : type.v : var- > exp.let : var- > exp- > exp- > exp .​​​​​​  
   
     
         

ここで、expはすべての式の型であり、varすべての組み込み変数の型です (おそらく自然数として実装されていますが、これは示されていません)。 定数 はvキャスト関数として機能し、変数が式であるという事実を証明します。 最後に、定数 は というlet形式の let 構造を表しますlet <var> = <exp> in <exp>。つまり、変数、式 (変数によってバインドされる)、および別の式 (変数がバインドされる) を受け入れます。

同じオブジェクト言語の 標準的なHOAS表現は次のようになります。

 exp : type.let : exp - > ( exp- > exp ) - > exp .  
         

この表現では、オブジェクトレベルの変数は明示的には現れません。定数はlet式（バインドされる）とメタレベルの関数exp→ exp （letの本体）を取ります。この関数は高階部分です。自由変数を持つ式は、適用時にメタレベルの関数によって埋められる穴のある式として表現されます。具体的な例として、オブジェクトレベルの式を構築します。

 x = 1 + 2をx + 3とする     
    

（数値と加算の自然な構成子を仮定）上記のHOASシグネチャを使用して

 let (プラス1 2 ) ([ y ]プラスy 3 )       

ここで、 は[y] e関数 の Twelf 構文です。 ${\displaystyle \lambda イエ}$

この特定の表現には、上記以外の利点もあります。たとえば、バインディングのメタレベルの概念を再利用することで、エンコーディングでは、定義や証明を必要とせずに、型保持置換などのプロパティを利用できます。このように、HOAS を使用すると、エンコーディングでのバインディングに関連する 定型コードの量を大幅に削減できます。

高階抽象構文は、一般に、オブジェクト言語変数が数学的な意味での変数として (つまり、あるドメインの任意のメンバーの代わりとして) 理解できる場合にのみ適用できます。これは多くの場合当てはまりますが、常に当てはまるとは限りません。たとえば、動的スコープの変数は数学変数のように動作しないため、 Lispの一部の方言で見られるような動的スコープの HOAS エンコードから得られる利点はありません。

• 一般化された代数データ型
• パラメトリック高階抽象構文 (PHOAS)

• J. Despeyroux、A. Felty、A. Hirschowitz (1995)。「Coq の高階抽象構文」。型付きラムダ計算とその応用。コンピュータ サイエンスの講義ノート。第 902 巻。pp. 124–138。doi : 10.1007 /BFb0014049。ISBN 978-3-540-59048-42006年8月30日時点のオリジナルよりアーカイブ。
• Martin Hofmann (1999)。高階抽象構文の意味分析。第 14 回IEEE コンピュータサイエンスにおける論理シンポジウム。p. 204。ISBN 0-7695-0158-3。
• Eli Barzilay、Stuart Allen (2002)。Nuprl での高階抽象構文の反映( PDF)。高階論理における定理証明2002。pp. 23–32。ISBN 3-540-44039-92006年10月11日時点のオリジナル（PDF）よりアーカイブ。
• Eli Barzilay (2006)。HOAS を使用したセルフホスティング評価ツール(PDF)。Schemeと関数型プログラミングに関するICFPワークショップ 2006。