Algebraic Semantics for Higher-Order Functional-Logic Programming
(高階関数論理型言語のための代数的意味論)

Makoto Hamana

Abstract

本論文では我々は高階関数論理プログラムの意味論を 型付き普遍代数の枠組みで与える. ここで考察する高階関数論理型言語は 作用型項書換え系($\lambda$ 計算の言葉で言えば, ユーザー定義のコンビネータのための$\delta$ 規則) の形をしており,$\lambda$ 抽象の機構は備わっていない. そのため,高階関数を含んだような質問の求解を, 従来の一階ナローイングの方法を使って解くことができるという利点がある. 我々は高階関数論理型言語の意味論として,型付きの代数を用い二つのモデルを与え る.この二つのモデルのうち,一つは始モデルとなる商項モデルであり,もう一 つは極小作用型エルブランモデルと呼ばれるものである.このモデルでは,プ ログラムは「高階関数の定義」,質問は「高階関数を含み得るような存在限量さ れた等式」として解釈される.高階関数論理型言語はデータとして関数を用いる ことができるため,この極小作用型エルブランモデルの台集合は,関数空間を含 むものとして構成される.質問の解は,このモデル中の要素のうち,質問をみた すものとして解釈される. ナローイングの健全性と完全性は,商項モデルと極小作用型エルブランモデルの 双方に対して示される. 作用型エルブランモデルの極小性―これは領域中のどんな要素 もある項の表示となっていることを表す―の要請は 作用型の関数論理プログラムにおいて, ナローイングの完全性を得るために必須な条件であることを示す.

Last modified: Tue Apr 29 05:45:41 JST 1997