Well, that’s not FOL, or it’s not a WFF anyway. It’s Prolog I think, and it won’t be done automatically either in FOL or in Prolog. In Prolog it will fail because the two sides of the = don’t unify. In FOL, I don’t know how to interpret the equality symbol.
I think what this means is that * and + are mapped to functions over objects in the domain of discourse, as would be done by a pre-interpretation according to some authors? Is that right?
Right. And Prolog, too. Prolog is not FOL 
What I wrote here is an axiom about equality = which
one cannot do in standard Prolog, but in FOL with
equality =, sometimes abreviated as FOL=, it is possible.
Most signatures do not explicitly mention the = relation:
Its not purely relational, it has function symbols. It is a well
formed formula WFF or sentence. Thats how FOL is
defined, you find another example here:
“For example, in an interpretation of first-order logic,
the domain of discourse is the set of individuals over
which the quantifiers range. A sentence such as ∀x (x^2 ≠ 2)
is ambiguous if no domain of discourse has been identified.”
https://en.wikipedia.org/wiki/Domain_of_discourse#Examples
The difference between FOL with equality =, and standard Prolog
is that Prolog equality is not FOL equality. Because you
cannot write axioms about equality = in standard Prolog.
But distributivity is exactly an axiom about equality =.
So how translate such an axiom into Prolog? Try this:
?- ord_union([a,b,c], [c,d,e], X),
ord_union([a,b,c], [a,e,f], Y),
ord_intersection(X, Y, Z).
Z = [a, b, c, e].
?- ord_intersection([c,d,e], [a,e,f], S),
ord_union([a,b,c], S, T).
T = [a, b, c, e].
So its quite useful to shorten programs and queries.
I think it depends on the author because in my sources that would not be a WFF, but I can see what you mean.
So there’s a definition of “distributivity” in terms of set operations?
You don’t find it in propositional logic (zero order logic). Since zero
order has anyway no domain of discourse. But in predicate logic
(first order logic) you find it:
"The next step is to define the atomic formulas.
Well-formed_formula Predicate_logic
https://en.wikipedia.org/wiki/Well-formed_formula#Predicate_logic
Now to your next questions:
These tiny sets are just a boolean algebra, with two
distributivity laws, both meet and join distribute:
Boolean algebra (structure)
https://en.wikipedia.org/wiki/Boolean_algebra_(structure)
Goes also by the name Boolean lattice. And for sets
it is sometimes more common to use ∪ , ∩ , etc.. typography.
But you might still need a “semi-” somewhere, since the
complement of {1,2,3} has no finite list representation in Prolog.
The use of =>/2 was introduced 5 years ago: History for library/ordsets.pl - SWI-Prolog/swipl-devel · GitHub but the change was quite minor.
Yes and no. A non-matching rule is a cheap and implicit message that typically translates to a domain, type or instantiation error. You have to get used to it but in most cases it is quite obvious what is wrong if you get such an exception. We might event try to be smart, look at the arguments and clauses and try to figure out why there is no match and come up with a better error message if we can.
Lets say I would have just won in the lottery and can
spend all my day improving Prolog. Now this looks
like a kind of a union type argument to me:
So in the above it would be [] or [_|_] expected. Maybe
must_be/2 provides a dictionary that this translates to list ?
So even without a type annotation somewhere by just
reading the (=>)/2 rules. But I didn’t win in a lottery. Also
it would not always be that simple with (=>)/2 rules.
I mean my sources for FOL. As you say FOL with equality is not the same as FOL. The definition of t1=t2 above makes = a predicate symbol which is what I always expected of FOL with equality, but to be honest I’ve never really looked into that because it never seems to crop up in logic programming or inductive logic programming work.
To be honest I’m not sure why it is important to define new logics whose whole schtick is that they have a special definition of a predicate, or more. Like all the modal logics for example, AFAIU them. That kind of specialisation seems to only serve the interest of having a subject to publish papers on.
You’ll find I’m a bit hardcore with sticking to FOL though, perhaps not completely reasonably so. For example I have never seen the point of any work in logic starting with Church and beyond. All of that seems like unnecessary over-engineering to me, and while I sorta see the motivation, my head just hurts every time I try to get it around e.g. the labmda calculus, or temporal logic, or whatever, and I keep thinking “I don’t need all this special notation, I can just do that with higher-order predicate logic”.
Yes! Unification is not equality. It’s really just a way to avoid grounding the entire Herbrand base of a predicate before a proof can be completed. In fact, it lets you postpone the grounding until the proof is complete. The alternative is … ASP. And while I’m fine with ASP, it’s got limitations that I wouldn’t want to see in Prolog (e.g. no lists or at least no natural notation for lists, although you can always hack in a sort of “list” representation).
Prolog always gets a bad rep for being inefficient with backtracking etc, but the grounding problem that has to be solved before executing an ASP problem is NP-complete. Oh and it doesn’t work with infinite Herbrand bases. I’m guessing that Robinson was well aware of that and was looking for a way to avoid the hassle.
EDIT: if I understand correctly the ASP “list” representation is as a set of dyadic atoms, where the first argument is an index and the second an element. So e.g. the list [a,b,c,d] becomes:
el(1,a).
el(2,b).
el(3,c).
el(4,d)
For a base-one list.
You know, I always forget the sources are on github and I can just look at them in my browser
It depends how precise you use mathematical logic terminology.
For everyday use, i.e. coarse grained terminology, FOL includes
always equality. For more technical work, like logic programming, i.e.
fine grained terminology, one might distinguish FOL- and FOL+.
FOL-:
Relational and functional first order logic. No notion of equality.
FOL+:
A notion of an equality relation = as well. For example by axioms:
Purer forms of Prolog share with FOL+ that unification also satisfies Reflexiv, Symmetric, Transitive and Congruences. But it has also Freeness of function symbols and the Occurs Check, which is not part of FOL+ per se:
Freeness:
∀x1 .. ∀xn ∀y1 .. ∀ym ( f(x1,..,xn) \= g(y1,..,ym) ) for f \= g or n \= m
Occurs Check:
∀y1 .. ∀ym ∀x ( x \= f(… x …) ) for y1,..,ym var of f(… x …)
But then comes Alain Colmerauer and Rational Trees. For example FOL+ and Herbrand inspired Prolog with occurs check doesn’t have the Alain Colmerauer existence of Cyclic Terms per se:
If you work without occurs check and can deal with cyclic terms you replace 7 by 8, which is a kind of inner opposite. This is what some Prolog systems in a sense effectively now do, i.e. SWI-Prolog, Scryer Prolog, Trealla Prolog, etc..
Hint: \= has to be read as negation as failure, like in the Clark Equational
theory. It indicates when unification fails and when we want a proof certificate
for some “UNSAT”, i.e. explainable AI, and not simply no proof.
Its interesting to see how Picat style (=>)/2 destroys this appeal:
The new Picat style (=>)/2 ordsets give:
?- ord_union([foo, bar], baz, X).
ERROR: No rule matches ordsets:union2(baz,foo,[bar],_168)
An old ordset implementation might have given:
?- ord_union([foo, bar], baz, X).
fail.
And we even didn’t look yet into the relationship of pattern matching
to FOL+. While the relationship of unification to FOL+ is relatively
straight forward, pattern matching does more than unification,
since it not only signals a type error, which an old implementation
of ord_union/3 would maybe propagate as failure. It also fiddles with a
non-logical var/1. We could translate union2/4 back into normal Prolog:
union2(V, _, _) :- var(V),
throw(error(instantiation_error,_)).
union2([], H1, T1, Union) :- !,
Union = [H1|T1].
union2([H2|T2], H1, T1, Union) :- !,
compare(Order, H1, H2),
union3(Order, H1, T1, H2, T2, Union).
union2(V, _, _) :-
throw(error(type_error(T,list),_)).
So what is the FOL+ equivalent of var/1. The type error is easier, it signals
this FOL+ axiom, short cutting a detailed proof of (\=)/2 that could have a
proof certification in an explainable AI, by throwing an error bomb for:
It seems an explainable AI Prolog has not yet been built. And picking
up Picat vibes, might make it even more difficult. But I might be mistaken,
since Picat was probably inspired by Haskell which has types. The interesting
challenge is to do explainable AI and not have types. At least this is an
idea that keeps me already awake for a couple of weeks.
It doesn’t need to be perfect. We can figure out for each argument which rules match and if a head matches which guard does not succeed. From there you could create a much more detailed report on why the predicate has no matching rules. Next, there are cases where this argument generalizes quite easily to a type/domain/instantiation error. I find myself quite often forgetting that => rules can not bind values in the head. Now I get no rule matching. It would be quite easy to say that what is intended to be an output argument suffers from an instantiation error. So, the idea would be
The benefit is clear: no pollution of your code and usable error messages.
Is there a Picat style (=>)/2 for if-then-else? Since this rule would bark,
when the comparator returns something outside of the 3 values
(<), (=) and (>), which is not extremly likely:
union3(<, H1, T1, H2, T2, Union) =>
Union = [H1|Union0],
union2(T1, H2, T2, Union0).
union3(=, H1, T1, _H2, T2, Union) =>
Union = [H1|Union0],
ord_union(T1, T2, Union0).
union3(>, H1, T1, H2, T2, Union) =>
Union = [H2|Union0],
union2(T2, H1, T1, Union0).
The semantic of a (=>)/2 if-then-else could be similar to a (=>)/2 rule.
If no condition succeeds, an error is thrown. I tested if-then-else without an
error branch, somehow a local if-then-else is ca. 10% faster, also shows
fewer inferences since I only used one predicate ord_union2/3:
?- time((test, fail; true)).
% 26,742,302 inferences, 0.516 CPU in 0.533 seconds
(97% CPU, 51863858 Lips)
true.
109 ?- time((test2, fail; true)).
% 16,780,318 inferences, 0.484 CPU in 0.478 seconds
(101% CPU, 34643237 Lips)
true.
Surprisingly Picat itself seems not to have an if-then-else with (=>)/2,
while its rather common in Haskell, for expressions, and generalizes
rules and local if-then-else somehow into one and the same pattern matching.
P.P.S.: Was using this, the if-then-else uses (->)/2, but an
if-then-else with (=>)/2 is also somehow conceivable.
ord_union2([], X, R) => R = X.
ord_union2(X, [], R) => R = X.
ord_union2([X|L], [Y|R], S) => compare(C, X, Y),
(C = (<) -> S = [X|T], ord_union2(L, [Y|R], T);
C = (=) -> S = [X|T], ord_union2(L, R, T);
C = (>) -> S = [Y|T], ord_union2([X|L], R, T)).
test2 :-
numlist(1,10, L),
numlist(1,10, R),
enum_subset(L, P),
enum_subset(R, Q),
ord_union2(P,Q,_).
That has been discussed when talking about => rules. It was never implemented. In part because of the now rather simple minded way => rules are implemented: they basically use normal unification and, after the head unification completes, it verifies that nothing is trailed, Using single-sided unification instructions would be more efficient, but also more complicated and adding more instructions tends to reduce performance (probably due to cache behaviour). Implementing => choice would be a lot easier using such instructions though.
Use C == (<) -> for speed. If-then-else condition evaluation is optimized for conditions that use no stack space and have no side effects such as a (partial) unification. In that case we do not need a choicepoint and we can simply evaluate the condition and jump (or not).