From Newsgroup: comp.lang.prolog

Hi,

Some people like Juglio post references to
wonderful meandering along terminology like:

If X has decidable equality and negation
of equality is an apartness relation, then
the negation of equality is a (in fact the
unique) decidable tight apartness relation
on X, and any function from X to any set
Y with a tight apartness relation on Y
must be strongly extensional.

https://ncatlab.org/nlab/show/strongly+extensional+function#examples

Still they are clueless how to sort rational
trees in Prolog. I am pretty sure such people
don't know how to do it practically in a Prolog system.

Bye

Julio Di Egidio schrieb:

In fact, how to constructive mathematics a la Bishop.

I haven't got to the bottom of it, it turns out to be
a long term project in itself, for both theoretical and
technical reasons, but here are few notes and mainly the
references that I have managed to collect.

"How to formalize dependent setoid morphisms?" <https://discourse.rocq-prover.org/t/2759>

To be continued...

-Julio

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

Hi,

Some precedent work in creating a notation
with sharing, is not only found in SWI-Prolog’s
term_factorized/3, but also in Ciao’s
Prolog uncycle_term/2:

uncycle_term(T,U)
Given a term T, U is a finite representation of T as an acyclic term. https://ciao-lang.org/ciao/build/doc/ciao.html/cyclic_terms.html#uncycle_term/2

Its even used in the Ciao Prolog debugger,
but I don’t know 100% whether it is used
for printing. Main take away from testing
the two top-levels:

- SWI-Prolog:
Uses internal term_factorized, possibly based on
same_term/2, so will still show X = f(f(X)) as such.

- Ciao Prolog:
Uses their uncycle_term/2, which is (==)/2 based,
so they can show X = f(f(X)) as X = f(X). But their
code has also a remark: slow!

But I guess the exclamation slow! might
be changed into a fast!, using some hash tables.
At least for a great deal of time, it would be faster.

Bye

Mild Shock schrieb:

Hi,

Some people like Juglio post references to
wonderful meandering along terminology like:

If X has decidable equality and negation
of equality is an apartness relation, then
the negation of equality is a (in fact the
unique) decidable tight apartness relation
on X, and any function from X to any set
Y with a tight apartness relation on Y
must be strongly extensional.

https://ncatlab.org/nlab/show/strongly+extensional+function#examples

Still they are clueless how to sort rational
trees in Prolog. I am pretty sure such people
don't know how to do it practically in a Prolog system.

Bye

Julio Di Egidio schrieb:

In fact, how to constructive mathematics a la Bishop.

I haven't got to the bottom of it, it turns out to be
a long term project in itself, for both theoretical and
technical reasons, but here are few notes and mainly the
references that I have managed to collect.

"How to formalize dependent setoid morphisms?" <https://discourse.rocq-prover.org/t/2759>

To be continued...

-Julio

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog


That anything printing could be also used
for sort, was maybe never explored, but is
evident when we seek a representation based
comparator, since printing is of course
also a representation.

Ciao Prologs uncycle_term/2 is realized
in 100% Prolog, just like my current
explorations. The source code is found on
GitHub. It doesn’t need some special built-in,

since it uses (==)/2 and not same_term/2:

:- module(cyclic_terms, ) https://github.com/ciao-lang/ciao/blob/fdff410cf2b7f2b85baff97485a2db5522d785f3/core/lib/cyclic_terms.pl

The latest comment was 5 years ago, “(core)
faster prettysols.pl (toplevel)”, but this only
refers to bypassing uncycle_term/2 in case of
an acyclic term. Otherwise it has a separate

uncycle_eqs, uncycle_val, etc.. implementation.
A little bit the same evolution that happend
in my Prolog system over the last days.

Mild Shock schrieb:

Hi,

Some precedent work in creating a notation
with sharing, is not only found in SWI-Prolog’s
term_factorized/3, but also in Ciao’s
Prolog uncycle_term/2:

uncycle_term(T,U)
Given a term T, U is a finite representation of T as an acyclic term. https://ciao-lang.org/ciao/build/doc/ciao.html/cyclic_terms.html#uncycle_term/2

Its even used in the Ciao Prolog debugger,
but I don’t know 100% whether it is used
for printing. Main take away from testing
the two top-levels:

- SWI-Prolog:
  Uses internal term_factorized, possibly based on
  same_term/2, so will still show X = f(f(X)) as such.

- Ciao Prolog:
  Uses their uncycle_term/2, which is (==)/2 based,
  so they can show X = f(f(X)) as X = f(X). But their
  code has also a remark: slow!

But I guess the exclamation slow! might
be changed into a fast!, using some hash tables.
At least for a great deal of time, it would be faster.

Bye

Mild Shock schrieb:

Hi,

Some people like Juglio post references to
wonderful meandering along terminology like:

If X has decidable equality and negation
of equality is an apartness relation, then
the negation of equality is a (in fact the
unique) decidable tight apartness relation
on X, and any function from X to any set
Y with a tight apartness relation on Y
must be strongly extensional.

https://ncatlab.org/nlab/show/strongly+extensional+function#examples

Still they are clueless how to sort rational
trees in Prolog. I am pretty sure such people
don't know how to do it practically in a Prolog system.

Bye

Julio Di Egidio schrieb:

In fact, how to constructive mathematics a la Bishop.
;
I haven't got to the bottom of it, it turns out to be
a long term project in itself, for both theoretical and
technical reasons, but here are few notes and mainly the
references that I have managed to collect.
;
"How to formalize dependent setoid morphisms?"
<https://discourse.rocq-prover.org/t/2759>
;
To be continued...
;
-Julio

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

Hi,

Its possibly a problem of epochs and communities,
while the Aho, Garey & Ullman (1972) paper doesn't
mention bisimulation.

Bisimulaton enters normalization, respectively
uncycle_term/2 for example here:

already_seen([(T,U)|_], Term, U) :-
T == Term, !.
already_seen([_|Ts], Term, U) :-
already_seen(Ts, Term, U).

:- module(cyclic_terms, )

https://github.com/ciao-lang/ciao/blob/fdff410cf2b7f2b85baff97485a2db5522d785f3/core/lib/cyclic_terms.pl

The bisimulation enters normalization in the
form of (==)/2. Since an implementation of (==)/2
is typically based on bisimulation.

Take this example:

X = f(g(f(g(X))))

In memory f,g,f,g might all sit at different
memory locations: X = f@1(g@2(f@3(g@4(X)))),
where @n shows the memory location n.

To figure out that X = f(g(X)) is enough
the already_seen/3 predicate has to decide
the following (==)/2 identity:

f@1(g@2(...)) == f@3(g@4(...))

Which in turn can be done with same_term/2
and bisimulation, if we would explicitly
program (==)/2 as well in 100% Prolog.

Bye

Mild Shock schrieb:

That anything printing could be also used
for sort, was maybe never explored, but is
evident when we seek a representation based
comparator, since printing is of course
also a representation.

Ciao Prologs uncycle_term/2 is realized
in 100% Prolog, just like my current
explorations. The source code is found on
GitHub. It doesn’t need some special built-in,

since it uses (==)/2 and not same_term/2:

:- module(cyclic_terms, ) https://github.com/ciao-lang/ciao/blob/fdff410cf2b7f2b85baff97485a2db5522d785f3/core/lib/cyclic_terms.pl

The latest comment was 5 years ago, “(core)
faster prettysols.pl (toplevel)”, but this only
refers to bypassing uncycle_term/2 in case of
an acyclic term. Otherwise it has a separate

uncycle_eqs, uncycle_val, etc.. implementation.
A little bit the same evolution that happend
in my Prolog system over the last days.

Mild Shock schrieb:

Hi,

Some precedent work in creating a notation
with sharing, is not only found in SWI-Prolog’s
term_factorized/3, but also in Ciao’s
Prolog uncycle_term/2:

uncycle_term(T,U)
Given a term T, U is a finite representation of T as an acyclic term.
https://ciao-lang.org/ciao/build/doc/ciao.html/cyclic_terms.html#uncycle_term/2


Its even used in the Ciao Prolog debugger,
but I don’t know 100% whether it is used
for printing. Main take away from testing
the two top-levels:

- SWI-Prolog:
   Uses internal term_factorized, possibly based on
   same_term/2, so will still show X = f(f(X)) as such.

- Ciao Prolog:
   Uses their uncycle_term/2, which is (==)/2 based,
   so they can show X = f(f(X)) as X = f(X). But their
   code has also a remark: slow!

But I guess the exclamation slow! might
be changed into a fast!, using some hash tables.
At least for a great deal of time, it would be faster.

Bye

Mild Shock schrieb:

Hi,

Some people like Juglio post references to
wonderful meandering along terminology like:

If X has decidable equality and negation
of equality is an apartness relation, then
the negation of equality is a (in fact the
unique) decidable tight apartness relation
on X, and any function from X to any set
Y with a tight apartness relation on Y
must be strongly extensional.

https://ncatlab.org/nlab/show/strongly+extensional+function#examples

Still they are clueless how to sort rational
trees in Prolog. I am pretty sure such people
don't know how to do it practically in a Prolog system.

Bye

Julio Di Egidio schrieb:

In fact, how to constructive mathematics a la Bishop.
;
I haven't got to the bottom of it, it turns out to be
a long term project in itself, for both theoretical and
technical reasons, but here are few notes and mainly the
references that I have managed to collect.
;
"How to formalize dependent setoid morphisms?"
<https://discourse.rocq-prover.org/t/2759>
;
To be continued...
;
-Julio

--- Synchronet 3.21a-Linux NewsLink 1.2