From b172413527bc41d467e7a484496ce71f97efef64 Mon Sep 17 00:00:00 2001 From: Dan Rose Date: Mon, 16 Jun 2025 00:48:45 -0500 Subject: [PATCH 1/3] Document some predicates in reif --- src/lib/reif.pl | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/lib/reif.pl b/src/lib/reif.pl index 55618e84e..19d8b166e 100644 --- a/src/lib/reif.pl +++ b/src/lib/reif.pl @@ -19,6 +19,17 @@ :- meta_predicate(if_(1, 0, 0)). +%% if_(Cond, IfTrue, IfFalse). +% Monotonic if-then-else construct for use with reified conditions. +% Rather than branching on whether a predicate simply succeeds as in `Cond -> IfTrue; IfFalse`, the condition is given as a *reified predicate*. +% i.e. a relation that emits the atom `true` or `false` as an output argument. +% +% Unlike `Cond -> _ ; _`: +% +% * The condition may be false in multiple ways. +% * The condition may be true in multiple ways. +% * Failure of the condition results in *no* solutions + if_(If_1, Then_0, Else_0) :- call(If_1, T), ( T == true -> call(Then_0) @@ -27,6 +38,12 @@ ; throw(error(instantiation_error, _)) ). +%% =(X, Y, T). +% Reified equality predicate. +% +% `=(X,Y,true)` succeeds if X, Y *could* unify +% `=(X,Y,false)` succeeds if X, Y *could* fail to unify + =(X, Y, T) :- ( X == Y -> T = true ; X \= Y -> T = false @@ -34,6 +51,12 @@ ; T = false, dif(X, Y) ). +%% dif(X, Y, T). +% Reified disequality predicate. +% +% `dif(X,Y,true)` succeeds if X, Y *could* fail to unify +% `dif(X,Y,false)` succeeds if X, Y *could* unify + dif(X, Y, T) :- =(X, Y, NT), non(NT, T). From cddec6f60f0eff58b0daf58442a42c89238d66a8 Mon Sep 17 00:00:00 2001 From: Dan Rose Date: Mon, 16 Jun 2025 01:21:49 -0500 Subject: [PATCH 2/3] Maybe less operationalizing language? --- src/lib/reif.pl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/reif.pl b/src/lib/reif.pl index 19d8b166e..42c8e77b9 100644 --- a/src/lib/reif.pl +++ b/src/lib/reif.pl @@ -22,7 +22,7 @@ %% if_(Cond, IfTrue, IfFalse). % Monotonic if-then-else construct for use with reified conditions. % Rather than branching on whether a predicate simply succeeds as in `Cond -> IfTrue; IfFalse`, the condition is given as a *reified predicate*. -% i.e. a relation that emits the atom `true` or `false` as an output argument. +% i.e. a relation with an additional argument which takes the value `true` or `false`. % % Unlike `Cond -> _ ; _`: % From bb8171d1c20f3283aab2945df6e89fc78c243655 Mon Sep 17 00:00:00 2001 From: Dan Rose Date: Mon, 16 Jun 2025 10:23:19 -0500 Subject: [PATCH 3/3] Better wording? --- src/lib/reif.pl | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/src/lib/reif.pl b/src/lib/reif.pl index 42c8e77b9..6eaa86e1d 100644 --- a/src/lib/reif.pl +++ b/src/lib/reif.pl @@ -1,5 +1,12 @@ /** Predicates from [*Indexing dif/2*](https://arxiv.org/abs/1607.01590). +The core trick that, unlike the traditional conditional `A -> B ; C`, +the branching condition is *not* provided as a complete goal. + +Rather, the branching condition is a "reified goal", +i.e. a term which is completed with an additional argument `T`, +representing its satisfaction (`T = true`) and refutation (`T = false`). + Example: ``` @@ -19,16 +26,14 @@ :- meta_predicate(if_(1, 0, 0)). -%% if_(Cond, IfTrue, IfFalse). -% Monotonic if-then-else construct for use with reified conditions. -% Rather than branching on whether a predicate simply succeeds as in `Cond -> IfTrue; IfFalse`, the condition is given as a *reified predicate*. -% i.e. a relation with an additional argument which takes the value `true` or `false`. -% -% Unlike `Cond -> _ ; _`: +%% if_(Cond_1, IfTrue, IfFalse). +% Monotonic if-then-else construct. % -% * The condition may be false in multiple ways. -% * The condition may be true in multiple ways. -% * Failure of the condition results in *no* solutions +% Unlike `Cond_0 -> IfTrue; IfFalse`, this is nondeterministic in the condition. +% `Cond` is expected to be a reified goal. +% e.g. `if_((A=1), _, _)` +% where the `=` above is NOT the `(=)/2` predicate, but rather the `(=)/3` predicate +% defined in this module. if_(If_1, Then_0, Else_0) :- call(If_1, T), @@ -43,6 +48,8 @@ % % `=(X,Y,true)` succeeds if X, Y *could* unify % `=(X,Y,false)` succeeds if X, Y *could* fail to unify +% Partially call as a branching condition in `if_/3`: +% `if_(A=B, IfTrue, IfFalse)` =(X, Y, T) :- ( X == Y -> T = true @@ -56,6 +63,8 @@ % % `dif(X,Y,true)` succeeds if X, Y *could* fail to unify % `dif(X,Y,false)` succeeds if X, Y *could* unify +% Partially call as a branching condition in `if_/3`: +% `if_(dif(A,B), IfTrue, IfFalse)` dif(X, Y, T) :- =(X, Y, NT),