Gather every matching value from a list of things — and be honest about what “every” means.
flat-map.pl · output · proof · check · try it in the playground
Imagine a small table of facts, each saying subject — property — value: a book has an author, a person has a phone number. Some subjects have one value, some have several, some have none.
Now: for a list of subjects, collect all their values for one property into a single flat list. Programmers call this a flat map.
What happens with a subject that has two values? One that has none? A property nobody uses?
Four facts, and a rule that walks the list:
t(s1, p1, o1).
t(s2, p1, o2).
t(s3, p1, o3).
t(s3, p1, o4).
% … two lines defining append
flat_map([], _, []).
flat_map([S|Subjects], P, Objects) :- findall(O, t(S, P, O), Here), flat_map(Subjects, P, Rest), append(Here, Rest, Objects).
true :+ flat_map([s1,s2,s3], p1, Objects).
true :+ flat_map([missing], p1, Objects).
true :+ flat_map([s1], p2, Objects).
findall gathers all values of one subject into a list, Here;
append joins two lists end to end.
flat_map([s1, s2, s3], p1, [o1, o2, o3, o4]).
flat_map([missing], p1, []).
flat_map([s1], p2, []).
s3 contributes two values, o3 and o4, in order.[], not an error.[] too.For the first answer, the proof records:
p1 values of s1: [o1] — collected by searching.p1 values of s2: [o2] — collected.p1 values of s3: [o3, o4] — collected.[] — fact 7.[o3, o4], then [o2], then [o1] in front — rules 5 and 6.[o1, o2, o3, o4] — rule 8.The checker matched 14 steps to their program lines. Verdict: checked_with_obligations.
The 5 obligations are all of the kind called collected: each claims a
list is the complete set of answers — for example, that s3 has exactly
[o3, o4] and missing has nothing at all. A proof can show each value is
there; “and there are no others” comes from Eyedia having searched
everything it knows. The checker records that as an obligation instead of
pretending to prove it.
It did confirm that nothing in the program or the proof contradicts any of the 5 lists.
An obligation is not a flaw; it is a label on the one kind of claim that depends on nothing else being known. If someone later adds a fact, the lists could change — and the report tells you exactly which lists those are.
If you need proof with no such promises, --strict-proof rejects any
certificate that leans on one. This one would fail that stricter test,
on exactly these 5 lists.
node bin/eyedia.js examples/flat-map.pl
node bin/eyedia.js --goal "flat_map([s3, s1], p1, Objects)" examples/flat-map.pl
The second gives [o3, o4, o1]: the order follows the subject list. Or open
it in the playground.
Add the fact t(s2, p1, o5). and run again: the first answer becomes
[o1, o2, o5, o3, o4].
“Here are all the matches” is a stronger statement than “here are some matches”. Eyedia gives you the answer and marks precisely where it relied on having seen everything — so you know what to recheck when the data grows.