Normally a test such as “is this even?” either succeeds or fails, and the
caller branches on that. A reified test instead returns true or
false as a value. Once conditions are values, filtering and partitioning
can be written once, in library(reif), and reused with any condition.
Run it in the playground · Source
Split the numbers 1 to 8 into evens and odds, and classify 4 and 7, without writing a separate filter or a separate if-then-else for each task.
“Reify” means to make something concrete: here the truth of a condition becomes an ordinary term that another predicate can receive and dispatch on.
:- use_module(library(reif)).
even_t(N, true) :- 0 is N mod 2, !.
even_t(_, false).
By convention, a predicate ending in _t takes one extra argument, the truth
value. even_t(4, T) gives T = true, and even_t(7, T) gives T = false.
answer(Evens, Odds, First, Second) :-
tfilter(even_t, [1, 2, 3, 4, 5, 6, 7, 8], Evens),
tpartition(even_t, [1, 2, 3, 4, 5, 6, 7, 8], _, Odds),
if_(even_t(4), First = even, First = odd),
if_(even_t(7), Second = even, Second = odd).
tfilter/3 keeps the elements whose condition is true; tpartition/4
splits a list into the true and false parts; if_/3 chooses a branch from
the reified value. All three are generic: pass a different _t predicate and
they work unchanged.
eyeprolog examples/reified-conditionals.pl
answer([2, 4, 6, 8], [1, 3, 5, 7], even, odd).
The evens and odds come out in their original order, and the two classifications agree with them.
eyeprolog --proof examples/reified-conditionals.pl
step(answer([2, 4, 6, 8], [1, 3, 5, 7], even, odd),
rule(3),
['Evens' = [2, 4, 6, 8], 'Odds' = [1, 3, 5, 7], 'First' = even, 'Second' = odd],
[tfilter(even_t, [1, 2, 3, 4, 5, 6, 7, 8], [2, 4, 6, 8]),
tpartition(even_t, [1, 2, 3, 4, 5, 6, 7, 8], [2, 4, 6, 8], [1, 3, 5, 7]),
if_(even_t(4), even = even, even = odd),
if_(even_t(7), odd = even, odd = odd)]).
One rule, four uses. Each use is a call to a library predicate, and each is recorded with its exact arguments and result.
condition('C1', resolution, ok, 1).
condition('C4', coverage, ok, 5).
obligation(builtin, theory_scoped, tfilter(even_t, [1, 2, 3, 4, 5, 6, 7, 8], [2, 4, 6, 8])).
obligation(builtin, theory_scoped, if_(even_t(7), odd = even, odd = odd)).
trusted(4).
verdict(checked_with_obligations).
The rule step checks. The four library calls cannot be recomputed in a clean
library context, because they call back into this program’s even_t/2. The
checker therefore lists them as obligations: correct if even_t/2 means
what it says, which the program itself defines.
greater_t(Limit, N, T) and use tfilter/3 to keep the numbers
above 5, without touching tfilter/3.if_(even_t(4), …) with the plain ( 0 is 4 mod 2 -> … ; … ).
What is lost when the condition is not a value?tpartition/4 to split a list of words by whether they start with a
vowel.Learn more in The Art of EyeProlog, Chapters 17 (logic and control) and 34 (control).