<div dir="ltr"><div class="gmail_default" style="font-family:monospace,monospace">'existential' indeed comes from Philosophy, in fact from Plato some</div><div class="gmail_default" style="font-family:monospace,monospace">two-and-a-half thousand years ago, not from existentialism.</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">All men are mortal.       (all X)(man(X) -> mortal(X))</div><div class="gmail_default" style="font-family:monospace,monospace">Some man has a hat.       (some Y)(man(Y) & has_hat(Y))</div><div class="gmail_default" style="font-family:monospace,monospace">Therefore</div><div class="gmail_default" style="font-family:monospace,monospace"> Some mortal has a hat.   (some Y)(mortal(X) & has_hat(Y))</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">(all X) is written (∀X) and pronounced "for all X"</div><div class="gmail_default" style="font-family:monospace,monospace">It's like a "and" over every possible value.<br></div><div class="gmail_default" style="font-family:monospace,monospace">(some Y) is written (∃Y) and pronounced "there exists a Y".</div><div class="gmail_default" style="font-family:monospace,monospace">It's like an "or" over every possible value.</div><div class="gmail_default" style="font-family:monospace,monospace">'</div><div class="gmail_default" style="font-family:monospace,monospace">That's basically it.  <br></div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">If you're interested in Philosophy, the Stanford Encyclopedia</div><div class="gmail_default" style="font-family:monospace,monospace">of Philosophy would have been a good place to start.  See</div><div class="gmail_default" style="font-family:monospace,monospace"><a href="https://plato.stanford.edu/entries/quantification/">https://plato.stanford.edu/entries/quantification/</a></div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">In plain terms, consider a space ship with three parts:</div><div class="gmail_default" style="font-family:monospace,monospace">:- type ship_part</div><div class="gmail_default" style="font-family:monospace,monospace">   ---> lander</div><div class="gmail_default" style="font-family:monospace,monospace">      ; living_quarters</div><div class="gmail_default" style="font-family:monospace,monospace">      ; engine.</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">:- pred touches(ship_part, ship_part).</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">touches(lander, lander).<br></div><div class="gmail_default" style="font-family:monospace,monospace">touches(lander, living_quarters).</div><div class="gmail_default" style="font-family:monospace,monospace">touches(living_quarters, lander).</div><div class="gmail_default" style="font-family:monospace,monospace">touches(living_quarters, living_quarters).</div><div class="gmail_default" style="font-family:monospace,monospace">touches(living_quarters, engine).</div><div class="gmail_default" style="font-family:monospace,monospace">touches(engine, living_quarters).</div><div class="gmail_default" style="font-family:monospace,monospace">touches(engine, engine).</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">% is it true that every part touches the living quarters?</div><div class="gmail_default" style="font-family:monospace,monospace">% (universally quantified variable)<br></div><div class="gmail_default" style="font-family:monospace,monospace">   all [Part] touches(Part, living_quarters)</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">% is there a part that does not touch the engine?</div><div class="gmail_default" style="font-family:monospace,monospace">% (existentially quantified variable)<br></div><div class="gmail_default" style="font-family:monospace,monospace">   some [Part] \+ touches(Part, engine)</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">% find me a part that touches the lander</div><div class="gmail_default" style="font-family:monospace,monospace">   touches(Part, lander)</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">It's basically that simple.  What kind of quantifier you use</div><div class="gmail_default" style="font-family:monospace,monospace">(if any) depends on what question you want the program to answer</div><div class="gmail_default" style="font-family:monospace,monospace">at that point.  <br></div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">This is not *complete* code, let alone tested.</div><div class="gmail_default" style="font-family:monospace,monospace"><br></div><div class="gmail_default" style="font-family:monospace,monospace">Now there are (waves hands) two kinds of variables in Mercury:</div><div class="gmail_default" style="font-family:monospace,monospace">DATA variables (variables that stand for data values at run time)</div><div class="gmail_default" style="font-family:monospace,monospace">TYPE variables (variables that stand for types).</div><div class="gmail_default" style="font-family:monospace,monospace">Both kinds can be quantified.  Existentially quantified type</div><div class="gmail_default" style="font-family:monospace,monospace">variables are rather useful, but you can go a long way in Mercury</div><div class="gmail_default" style="font-family:monospace,monospace">without needing to worry about them.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 24 Oct 2023 at 02:38, Sean Charles (emacstheviking) <<a href="mailto:objitsu@gmail.com">objitsu@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">What areas of maths / logic do I need to study to better understand the Mercury compiler?<br>
<br>
I have a brain, so I have a chance.<br>
<br>
What I find mostly confusing is all the talk of 'existential' things, from philosophy I know what Existentialism means but not when applied to a language like Mercury. Also I still struggle with modes/inst and 'and-or' trees. I read the Wikipedia page on those until it stopped making sense (didn't take long), I have rough idea of what the Mercury manual is trying to tell me but I am sick and tired of feeling like a semi-educated simpleton and need to up my game.<br>
<br>
When I learned Prolog, I did some study about Horne clauses, and some other related subjects but only enough really to understand what I was doing at the time time, and it got me further down the road.<br>
<br>
But...Mercury. What a beast!   I truly want to get to know it's inner dialogue as it once again is forced to eat my probably horrendous code over and over.<br>
<br>
So... any topic for self-study would be most appreciated.<br>
<br>
<br>
_______________________________________________<br>
users mailing list<br>
<a href="mailto:users@lists.mercurylang.org" target="_blank">users@lists.mercurylang.org</a><br>
<a href="https://lists.mercurylang.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.mercurylang.org/listinfo/users</a><br>
</blockquote></div>