From Newsgroup: sci.logic


Struggle understanding Hopcroft and Karp (1971) ?
No worries Philip Zucker is the man:

Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas
You can make egraphs support stream like things / rational terms. https://www.philipzucker.com/coegraph/

Strange I came up with the same stuff over the last
weeks while discussing with @kuniaki.mukai .

Lets say 2025 is the year of rational trees!

Mild Shock schrieb:

Concerning this boring nonsense:

https://book.simply-logical.space/src/text/2_part_ii/5.3.html#

Funny idea that anybody would be interested just now in
the year 2025 in things like teaching breadth first
search versus depth first search, or even be rCLmystifiedrCY
by such stuff. Its extremly trivial stuff:

Insert your favorite tree traversal pictures here.

Its even not artificial intelligence neither has anything
to do with mathematical logic, rather belongs to computer
science and discrete mathematics which you have in
1st year university

courses, making it moot to call it rCLsimply logicalrCY. It
reminds me of the idea of teaching how wax candles work
to dumb down students, when just light bulbs have been
invented. If this is the outcome

of the Prolog Education Group 2.0, then good night.

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.logic

Hi,

Using Hopcroft & Karp (HK) everywhere
clearly raises the bar. I decided to use
HK also in compare/3 , just to have it

detect structure sharing. But here a little
test comparing with WebPL, only (=)/2 because
I didn't find compare/3:

/* WebPL May 2025 */
test(25).
True
(1040.4ms)
https://webpl.whenderson.dev/

/* Dogelog Player 1.3.6 */
:- version.
:- time(test(25)).
Dogelog Spieler, Prolog zum Mond, 1.3.6 (02.08.2025)
(c) 1985-2025, XLOG Technologies AG, Schweiz
% Zeit 1 ms, GC 0 ms, Lips 125000, Uhr 14.08.2025 12:30 https://www.dogelog.ch/littab/doclet/live/07_basic/example01/package.html

SWI-Prolog WASM can also do it fast. The
old Trealla WASM version cannot do it fast.

Bye

P.S.: The test code:

hydra(0,_) :- !.
hydra(N,s(X,X)) :- M is N-1, hydra(M,X).

test(N) :-
hydra(N,X), hydra(N,Y), X = Y.

Mild Shock schrieb:

Struggle understanding Hopcroft and Karp (1971) ?
No worries Philip Zucker is the man:

Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas
You can make egraphs support stream like things / rational terms. https://www.philipzucker.com/coegraph/

Strange I came up with the same stuff over the last
weeks while discussing with @kuniaki.mukai .

Lets say 2025 is the year of rational trees!

Mild Shock schrieb:

Concerning this boring nonsense:

https://book.simply-logical.space/src/text/2_part_ii/5.3.html#

Funny idea that anybody would be interested just now in
the year 2025 in things like teaching breadth first
search versus depth first search, or even be rCLmystifiedrCY
by such stuff. Its extremly trivial stuff:

Insert your favorite tree traversal pictures here.

Its even not artificial intelligence neither has anything
to do with mathematical logic, rather belongs to computer
science and discrete mathematics which you have in
1st year university

courses, making it moot to call it rCLsimply logicalrCY. It
reminds me of the idea of teaching how wax candles work
to dumb down students, when just light bulbs have been
invented. If this is the outcome

of the Prolog Education Group 2.0, then good night.

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.logic

Hi,

This is a nice confusion of the highest order.

observations on the decidability

Well in summary the existence of a pretest (==)/2
makes Mercio's decidable. Equality on rational trees
is decidable, even if it comes in disguise as MerciorCOs
mathematical definition, which gives a total order

which is unfortunately not a natural order:

A=B :rf| A' =lex B'

A<B :rf| A' <lex B'

Natural order of rational trees?
https://math.stackexchange.com/a/210730

Why is MerciorCOs mathematical definition of equality
decidable? Because it is semantically equivalent to
bisimulation as implemented in (==)/2 , and decidable
is a semantic notion:

Decidability (logic)
In logic, a true/false decision problem is decidableif there
exists an effective method for deriving the correct answer.
Decidability (logic) - Wikipedia

So if you talk about semi-decidable, decidable etc..
its always about the existence of an algorithm in
the large space of effective method according to
the Church hypothesis.

If you want to talk about a particular algorithm
you would use the terminology rCLincompleterCY. Like for
example DFS algorithms are rCLincompleterCY compared to
BFS algorithms on certain problems.

Bye

Mild Shock schrieb:

Hi,

Using Hopcroft & Karp (HK) everywhere
clearly raises the bar. I decided to use
HK also in compare/3 , just to have it

detect structure sharing. But here a little
test comparing with WebPL, only (=)/2 because
I didn't find compare/3:

/* WebPL May 2025 */
test(25).
True
(1040.4ms)
https://webpl.whenderson.dev/

/* Dogelog Player 1.3.6 */
:- version.
:- time(test(25)).
Dogelog Spieler, Prolog zum Mond, 1.3.6 (02.08.2025)
(c) 1985-2025, XLOG Technologies AG, Schweiz
% Zeit 1 ms, GC 0 ms, Lips 125000, Uhr 14.08.2025 12:30 https://www.dogelog.ch/littab/doclet/live/07_basic/example01/package.html

SWI-Prolog WASM can also do it fast. The
old Trealla WASM version cannot do it fast.

Bye

P.S.: The test code:

hydra(0,_) :- !.
hydra(N,s(X,X)) :- M is N-1, hydra(M,X).

test(N) :-
-a-a hydra(N,X), hydra(N,Y), X = Y.

Mild Shock schrieb:

Struggle understanding Hopcroft and Karp (1971) ?
No worries Philip Zucker is the man:

Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas
You can make egraphs support stream like things / rational terms.
https://www.philipzucker.com/coegraph/

Strange I came up with the same stuff over the last
weeks while discussing with @kuniaki.mukai .

Lets say 2025 is the year of rational trees!

Mild Shock schrieb:

Concerning this boring nonsense:

https://book.simply-logical.space/src/text/2_part_ii/5.3.html#

Funny idea that anybody would be interested just now in
the year 2025 in things like teaching breadth first
search versus depth first search, or even be rCLmystifiedrCY
by such stuff. Its extremly trivial stuff:

Insert your favorite tree traversal pictures here.

Its even not artificial intelligence neither has anything
to do with mathematical logic, rather belongs to computer
science and discrete mathematics which you have in
1st year university

courses, making it moot to call it rCLsimply logicalrCY. It
reminds me of the idea of teaching how wax candles work
to dumb down students, when just light bulbs have been
invented. If this is the outcome

of the Prolog Education Group 2.0, then good night.

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.logic

Hi,

This is a nice confusion of the highest order.

observations on the decidability

Well in summary the existence of a pretest (==)/2
makes Mercio's decidable. Equality on rational trees
is decidable, even if it comes in disguise as MerciorCOs
mathematical definition, which gives a total order

which is unfortunately not a natural order:

A=B :rf| A' =lex B'

A<B :rf| A' <lex B'

Natural order of rational trees?
https://math.stackexchange.com/a/210730

Why is MerciorCOs mathematical definition of equality
decidable? Because it is semantically equivalent to
bisimulation as implemented in (==)/2 , and decidable
is a semantic notion:

Decidability (logic)
In logic, a true/false decision problem is decidableif there
exists an effective method for deriving the correct answer.
Decidability (logic) - Wikipedia

So if you talk about semi-decidable, decidable etc..
its always about the existence of an algorithm in
the large space of effective method according to
the Church hypothesis.

If you want to talk about a particular algorithm
you would use the terminology rCLincompleterCY. Like for
example DFS algorithms are rCLincompleterCY compared to
BFS algorithms on certain problems.

Bye

Mild Shock schrieb:

Hi,

Using Hopcroft & Karp (HK) everywhere
clearly raises the bar. I decided to use
HK also in compare/3 , just to have it

detect structure sharing. But here a little
test comparing with WebPL, only (=)/2 because
I didn't find compare/3:

/* WebPL May 2025 */
test(25).
True
(1040.4ms)
https://webpl.whenderson.dev/

/* Dogelog Player 1.3.6 */
:- version.
:- time(test(25)).
Dogelog Spieler, Prolog zum Mond, 1.3.6 (02.08.2025)
(c) 1985-2025, XLOG Technologies AG, Schweiz
% Zeit 1 ms, GC 0 ms, Lips 125000, Uhr 14.08.2025 12:30 https://www.dogelog.ch/littab/doclet/live/07_basic/example01/package.html

SWI-Prolog WASM can also do it fast. The
old Trealla WASM version cannot do it fast.

Bye

P.S.: The test code:

hydra(0,_) :- !.
hydra(N,s(X,X)) :- M is N-1, hydra(M,X).

test(N) :-
-a-a hydra(N,X), hydra(N,Y), X = Y.

Mild Shock schrieb:

Struggle understanding Hopcroft and Karp (1971) ?
No worries Philip Zucker is the man:

Co-Egraphs: Streams, Unification, PEGs, Rational Lambdas
You can make egraphs support stream like things / rational terms.
https://www.philipzucker.com/coegraph/

Strange I came up with the same stuff over the last
weeks while discussing with @kuniaki.mukai .

Lets say 2025 is the year of rational trees!

Mild Shock schrieb:

Concerning this boring nonsense:

https://book.simply-logical.space/src/text/2_part_ii/5.3.html#

Funny idea that anybody would be interested just now in
the year 2025 in things like teaching breadth first
search versus depth first search, or even be rCLmystifiedrCY
by such stuff. Its extremly trivial stuff:

Insert your favorite tree traversal pictures here.

Its even not artificial intelligence neither has anything
to do with mathematical logic, rather belongs to computer
science and discrete mathematics which you have in
1st year university

courses, making it moot to call it rCLsimply logicalrCY. It
reminds me of the idea of teaching how wax candles work
to dumb down students, when just light bulbs have been
invented. If this is the outcome

of the Prolog Education Group 2.0, then good night.

--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.logic

Hi,

DFS algorithms can nevertheless gain some completness
power on rational trees when paired with loop checking.
Like @kuniaki.mukai was using in compare_with_stack/3.
They might be not as good as HK though.

You find a DFA subset and equality relation here,
implemented via DFS algorithms using a visitor set:

def find_equiv_counterexample(dfa_a, dfa_b):
# Symmetric difference: strings accepted by exactly one DFA
return find_word(dfa_a ^ dfa_b)

def find_subset_counterexample(smaller, bigger):
# Intersection of "smaller" with the complement of "bigger"
return find_word(~bigger & smaller)

https://pypi.org/project/dfa/

The later results in ordering DFAs by a partial order
and not by a total order. The project has also a DFA
minimization algorithm. But I didnrCOt get my head around
yet implementing it,

and I donrCOt know whether @kuniaki.mukai implemented
the DFA minimization algorithm that has supposedly
O(N log(N)) complexity.

Bye

Mild Shock schrieb:

Hi,

This is a nice confusion of the highest order.

observations on the decidability

Well in summary the existence of a pretest (==)/2
makes Mercio's decidable. Equality on rational trees
is decidable, even if it comes in disguise as MerciorCOs
mathematical definition, which gives a total order

which is unfortunately not a natural order:

A=B :rf| A' =lex B'

A<B :rf| A' <lex B'

Natural order of rational trees?
https://math.stackexchange.com/a/210730

Why is MerciorCOs mathematical definition of equality
decidable? Because it is semantically equivalent to
bisimulation as implemented in (==)/2 , and decidable
is a semantic notion:

Decidability (logic)
In logic, a true/false decision problem is decidableif there
exists an effective method for deriving the correct answer.
Decidability (logic) - Wikipedia

So if you talk about semi-decidable, decidable etc..
its always about the existence of an algorithm in
the large space of effective method according to
the Church hypothesis.

If you want to talk about a particular algorithm
you would use the terminology rCLincompleterCY. Like for
example DFS algorithms are rCLincompleterCY compared to
BFS algorithms on certain problems.

Bye

--- Synchronet 3.21a-Linux NewsLink 1.2