ローカル述語

💡 お知らせ: このドキュメントはAIによって翻訳されています。表現に違和感がある場合は、原文（英語）を参照するか、翻訳にご協力ください。

Flix は、local predicates(ローカル述語) と呼ばれる抽象化の仕組みをサポートしています。ローカル述語は、ローカル変数と同じように、外部からは見えません。

ローカル述語を理解するために、次の例を考えてみましょう。グラフに閉路があるかどうかを計算する Datalog プログラム値を返す関数を書くことができます：

def cyclic(): #{Edge(Int32, Int32), Path(Int32, Int32), Cyclic()} = #{
    Path(x, y) :- Edge(x, y).
    Path(x, z) :- Path(x, y), Edge(y, z).
    Cyclic() :- Path(x, x).
}

def main(): Unit \ IO = 
    let db = #{
        Edge(1, 2).
        Edge(2, 3).
        Edge(3, 1).
    };
    query db, cyclic() select true from Cyclic() |> println

ここで cyclic 関数は、辺からなるグラフの推移閉包と、ある頂点からその頂点自身への経路が存在するかどうかを計算する 3 つのルールで構成された、Datalog program value(Datalog プログラム値) を返します。main の中で cyclic 関数を使って、db で与えられる小さなグラフに閉路があるかどうかを判定しています。このプログラムをコンパイルして実行すると、Vector#{true} が出力されます。

cyclic に話を戻すと、その型は次のようになっています：

def cyclic(): #{Edge(Int32, Int32), Path(Int32, Int32), Cyclic()} = ...

この Datalog プログラム値は述語シンボル Edge、Path、Cyclic をそれぞれの型で使用しているので、この型は妥当です。しかし、もう少し考えてみると、Path 述語は実際にはこの計算にとってローカルなものであることに気づきます。外部から見えることを意図したものではなく、実装の詳細なのです！本当に望ましいのは、Edge(Int32, Int32) が入力であり、Cyclic() が出力であることです。さらに重要なのは、Path(Int32, Int32) は外部から見えてはならず、型の一部であってもならないということです。これは predicate abstraction(述語抽象) によって実現できます：

def cyclic(): #{Edge(Int32, Int32), Cyclic()} = 
    #(Edge, Cyclic) -> #{
        Path(x, y) :- Edge(x, y).
        Path(x, z) :- Path(x, y), Edge(y, z).
        Cyclic() :- Path(x, x).
    }

ここでは #(Edge, Cyclic) -> v という構文を使って、v の中の述語のうち Edge と Cyclic だけを外部から見えるようにすることを指定しています。これにより、cyclic の戻り値の型から Path(Int32, Int32) を省略できます。さらに、この Datalog プログラム値には、参照可能な Path 述語シンボルはもはや含まれていません。このことは、次のプログラムを観察することで確かめられます：

def main(): Unit \ IO = 
    let db = #{
        Edge(1, 2).
        Edge(2, 3).
        Edge(3, 1).
    };
    query db, cyclic() select (x, y) from Path(x, y) |> println

このプログラムは空のベクター Vector#{} を出力します。述語抽象によって Path がローカルになっているためです。

Keyboard shortcuts

Programming Flix

ローカル述語