This is a topic to discuss the Wiki
I take it the idea is to write a new, better version of the documentation page for =/2, explaining what unification is and how it works here?
The idea is not to replace it, but create a Wiki page on Unification that will remain here that other places can link to including the SWI-Prolog documentation. In hanging out at the StackOverflow Prolog tag for some years many people new to Prolog hit basic unification problems and I really never had a good link to give them to help them learn and really didnāt want to write a few pages just to answer their question so more than not I would just not answer other than a comment to the Wikipedia section on syntactic unification which I know was not much if any help, but at least they had more than when they asked.
I have some ideas on what to do, but donāt want to come on strong at the beginning and chase people away.
Any ideas and suggestions you have are welcome and the reason the Wikis are made a Wiki type topic is so that any Basic user here can go in and change it, just click on the pencil in the lower right. If anyone does something that is not desired the topics here have history that can be reverted. So edit away, I would be pleased to see others join in and help.
Personal notes (Click triangle to expand)
Prolog and Infinite Trees by Alain Colmerauer
Comments for cyclic terms in pl-prims.c
1 Like
I added some examples but I am not satisfied with the layout of the images. In the original HTML from which this was copied the images line up under the query and are done using <img src=... > tags where the source is in a subdirectory the html directory. I think discourse can do it if one has admin rights. Any way that is the best I can do at the moment. Also the true and false values are color coded, but that is not showing up as expected.
ā is not being recognized as a variable so queries like this =(ā,ā). are failing.
?- char_type('A',Type).
Type = alnum ;
Type = alpha ;
Type = csym ;
Type = csymf ;
Type = prolog_var_start ;
Type = prolog_identifier_continue ;
Type = csymf ;
Type = ascii ;
Type = graph ;
Type = upper ;
Type = upper(a) ;
Type = to_lower('A') ;
Type = to_upper(a) ;
Type = xdigit(10)
?- char_type('ā',Type).
Type = prolog_symbol ;
Type = to_lower(ā) ;
Type = to_upper(ā) ;
false.
Possible alternatives to the characters ā ā ā
C = 'Ī',
Types = [alnum, alpha, csym, csymf, prolog_var_start, prolog_identifier_continue, csymf, graph, upper|...],
Code = 920 ;
Code: 0x399
C = 'Š§',
Types = [alnum, alpha, csym, csymf, prolog_var_start, prolog_identifier_continue, csymf, graph, upper|...],
Code = 1063 ;
Code: 0x428
C = 'ā°',
Types = [alnum, alpha, csym, csymf, prolog_var_start, prolog_identifier_continue, csymf, graph, upper|...],
Code = 11294 ;
Code: 0x2C1F
Due to the formatting constraints with Discourse Markdown I am considering putting this into a PDF and then posting the link in the Wiki.
EDIT
This CSS option with Discourse might solve the problem.
Found out that HTML can use SVG as an island grammar. See: Inline SVG example
Need to add part about Prolog flag for occurs check and allow_variable_name_as_functor
1 Like
This is unrelated to unification. It is a mere syntax extension that was once added to deal with some domain specific language project. The var_prefix flag is more promising for such cases while we also have quasi quotations.
2 Likes
Thanks,
I didnāt think you were reading these as I wrote them, but glad you are.
Warrenās Abstract Machine - A TUTORIAL RECONSTRUCTION
See: Chapter 2 - UnificationāPure and Simple
One thing is lacking there: unification of cyclic terms (or infinite trees). This works (not in all Prolog systems though):
?- X = f(X), Y = f(Y), X = Y.
X = Y, Y = f(Y).
1 Like
I didnāt know that was possible. Something more for me to learn about. Thanks.
You may also want to do a web search for ārational treesā (I think this terminology is from Prolog II).
e.g. https://www.swi-prolog.org/pldoc/man?section=cyclic
https://dtai.cs.kuleuven.be/projects/ALP/newsletter/archive_93_96/net/impl/occur.html
More specifically:
I knew that X=Y was possible.
I knew that X=f(X) and Y=f(Y) was possible if the occurs check was not being applied.
But when I look at X = f(X), Y = f(Y), X = Y.
I think X is unified with f(X) and Y is unified with f(Y) by lack of occurs check, but then I stop the unification process in my head because I donāt think there is more, but obviously there is because the MGU does not include X = f(X) which if this were a test I would have answered wrong or been very confused and probably not have given a correct answer unless it was multiple choice upon which I could have reasoned that there was an answer I wasnāt expecting and it would have been a correct answer.
After X=f(X) and Y=f(Y) you end up with two identical cyclic terms. You want unification to succeed, but if you do the good old naive unification you go into infinite recursion (or loop if you apply last argument optimization). I learned how to deal with this from Bart Demoen. It is described in the sources.
1 Like
See: GitHub SWI-Prolog/swipl-devel - Cyclic Terms
I donāt know how I forgot to add this earlier.
Unification theory - Chapter 8 of Handbook of Automated Reasoning (WorldCat)
Thereās also one-way unification, otherwise known as pattern-matching. (Erlang, ML, Python use various flavors of pattern-matching)
This might help a bit (I havenāt read through it all ā¦ thereās some discussion about linear and non-linear pattern matching, which is terminology Iām not familiar with):
And donāt forget subsumption, which is important for tabling. 
[Do a web search for subsumption unification and have fun ā¦]
1 Like
On the topic of subsumption, itās useful to know that subsumes_term/2 was added to ISO Prolog in Corrigendum 2 in 2012. The draft can be found here.
Subsumption is also very important in inductive logic programming. A clause A implies a clause B if (but not only if) A subsumes B. Subsumption is much easier to āinvertā than general implication.
1 Like
As much as I want to work on adding to the Wiki topics here, my main hold back is that using links in HTML to other files such as SVG is still a problem because of Discourse.
In using SWISH it seems that I can at least enter an HTML cell and use inline SVG (example).
Also it seems that I can create an HTML iframe bringing the SWISH page right into a Discourse topic.
So this is a test.
First a Google map to the Eiffel Tower in an iframe
Note: IFrame HTML deleted because the iframe updates every few seconds and causes a scroll of the post. Use history to see the IFrame HTML if desired.
second a use of CodePen without any HTML attributes
Note: IFrame HTML deleted because the iframe updates every few seconds and causes a scroll of the post. Use history to see the IFrame HTML if desired.
and now an iframe for the SWISH page.
Note: IFrame HTML deleted because the iframe updates every few seconds and causes a scroll of the post. Use history to see the IFrame HTML if desired.
Not the greatest, but at least it worked.
Donāt count on the feature staying around as this was only a test and while it did work, it doesnāt seem to be practical. Will work on it some more, but donāt count on this as a permanent option just yet.
Using the iframe attributes width="600" height="450" frameborder="0" style="border:0" allowfullscreen
Played with this some here but then switched to use Discourse demo.
In trying to get the iframe for SWISH to be wider, (full width) ran into more issues with Discourse.
Instead of creating multiple replies, I am just adding any links that may be of value in trying to solve this problem into this one reply.
How to increase width of topic
Css to hide topic timeline per topic
Shadowboxes for IFRAMEs (SOLVED)
Iframe Lightboxes
Bind iframe height to its content height with jQuery
Custom Layouts Plugin
Jsfiddle-like embeds?
Support for Jupyter notebooks
A Quiet Desert Sunset - Themes can be specific to a category
Now I know why people are making a full time living as Discourse consultants.
At this point just doing the fancy stuff in SWISH looks more promising and just posting a link from the Wiki page to SWISH.
So if you saw the SWISH iframe working here for a few minutes and now it fails, it was because I first enabled the feature then disabled it. 