[m-users.] Self-improvement subjects.

[Richard O'Keefe]

'existential' indeed comes from Philosophy, in fact from Plato some
two-and-a-half thousand years ago, not from existentialism.

All men are mortal.       (all X)(man(X) -> mortal(X))
Some man has a hat.       (some Y)(man(Y) & has_hat(Y))
Therefore
 Some mortal has a hat.   (some Y)(mortal(X) & has_hat(Y))

(all X) is written (∀X) and pronounced "for all X"
It's like a "and" over every possible value.
(some Y) is written (∃Y) and pronounced "there exists a Y".
It's like an "or" over every possible value.
'
That's basically it.

If you're interested in Philosophy, the Stanford Encyclopedia
of Philosophy would have been a good place to start.  See
https://plato.stanford.edu/entries/quantification/

In plain terms, consider a space ship with three parts:
:- type ship_part
   ---> lander
      ; living_quarters
      ; engine.

:- pred touches(ship_part, ship_part).

touches(lander, lander).
touches(lander, living_quarters).
touches(living_quarters, lander).
touches(living_quarters, living_quarters).
touches(living_quarters, engine).
touches(engine, living_quarters).
touches(engine, engine).

% is it true that every part touches the living quarters?
% (universally quantified variable)
   all [Part] touches(Part, living_quarters)

% is there a part that does not touch the engine?
% (existentially quantified variable)
   some [Part] \+ touches(Part, engine)

% find me a part that touches the lander
   touches(Part, lander)

It's basically that simple.  What kind of quantifier you use
(if any) depends on what question you want the program to answer
at that point.

This is not *complete* code, let alone tested.

Now there are (waves hands) two kinds of variables in Mercury:
DATA variables (variables that stand for data values at run time)
TYPE variables (variables that stand for types).
Both kinds can be quantified.  Existentially quantified type
variables are rather useful, but you can go a long way in Mercury
without needing to worry about them.

On Tue, 24 Oct 2023 at 02:38, Sean Charles (emacstheviking) <
objitsu at gmail.com> wrote:

> What areas of maths / logic do I need to study to better understand the
> Mercury compiler?
>
> I have a brain, so I have a chance.
>
> 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.
>
> 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.
>
> 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.
>
> So... any topic for self-study would be most appreciated.
>
>
> _______________________________________________
> users mailing list
> users at lists.mercurylang.org
> https://lists.mercurylang.org/listinfo/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mercurylang.org/archives/users/attachments/20231024/1655615b/attachment-0001.html>