After years of enduring abominations such as
inappropriate use of DCG, pillow web servers and
Protobufs, leading to a down spiral
of turning Prolog into a bash scripting language
with further unholy marriages such as Prolog dicts
that are always closed or (=>)/2 for SSU,
there is finally a new book that mentions logic
programming in connection with Artificial intelligence.
Disclaimer, didn't read yet, but the context
looks interesting:
A Guided Tour of Artificial Intelligence Research - May, 2020
Logic Programming Pages 83-113 Lallouet, Arnaud (et al.) https://www.springer.com/gp/book/9783030061661
If you want to find the secret river, join the fire nation:
Aang Infiltrates a Fire Nation School https://www.youtube.com/watch?v=hu40eO7ox8w
LoL
So will the earth benders ever write efficient code? The fire
nation or the water benders could be ahead of their time,
but what about the earth benders?
Here is a DCG code smell:
% When Type is a variable, backtracks through all the possibilities
% for a given wire encoding.
[...]
prolog_type(Tag, unsigned64) --> protobuf_tag_type(Tag, fixed64). prolog_type(Tag, float) --> protobuf_tag_type(Tag, fixed32).
prolog_type(Tag, integer32) --> protobuf_tag_type(Tag, fixed32). prolog_type(Tag, unsigned32) --> protobuf_tag_type(Tag, fixed32). prolog_type(Tag, integer) --> protobuf_tag_type(Tag, varint).
[...]
Looks nice, but doesn't work. It can lead to spurious choice
points. This is a widespread inappropriate use of DCG. It is
declarative and logically correct, good for academic slides.
But not for production code.
Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 15:48:24 UTC+2:
The opposite evil of turning Prolog into a bash scripting
language is the motto use CLP(FD) everywhere and the
library(reif). Didn't fullfil any of its promisses either.
Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 15:41:44 UTC+2:
After years of enduring abominations such as
inappropriate use of DCG, pillow web servers and
Protobufs, leading to a down spiral
of turning Prolog into a bash scripting language
with further unholy marriages such as Prolog dicts
that are always closed or (=>)/2 for SSU,
there is finally a new book that mentions logic
programming in connection with Artificial intelligence.
Disclaimer, didn't read yet, but the context
looks interesting:
A Guided Tour of Artificial Intelligence Research - May, 2020
Logic Programming Pages 83-113 Lallouet, Arnaud (et al.) https://www.springer.com/gp/book/9783030061661
If you want to find the secret river, join the fire nation:
Aang Infiltrates a Fire Nation School https://www.youtube.com/watch?v=hu40eO7ox8w
LoL
The opposite evil of turning Prolog into a bash scripting
language is the motto use CLP(FD) everywhere and the
library(reif). Didn't fullfil any of its promisses either.
Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 15:41:44 UTC+2:
After years of enduring abominations such as
inappropriate use of DCG, pillow web servers and
Protobufs, leading to a down spiral
of turning Prolog into a bash scripting language
with further unholy marriages such as Prolog dicts
that are always closed or (=>)/2 for SSU,
there is finally a new book that mentions logic
programming in connection with Artificial intelligence.
Disclaimer, didn't read yet, but the context
looks interesting:
A Guided Tour of Artificial Intelligence Research - May, 2020
Logic Programming Pages 83-113 Lallouet, Arnaud (et al.) https://www.springer.com/gp/book/9783030061661
If you want to find the secret river, join the fire nation:
Aang Infiltrates a Fire Nation School https://www.youtube.com/watch?v=hu40eO7ox8w
LoL
The Kissat SAT solver is a reimplementation of CaDiCaL in C. https://twitter.com/ArminBiere/status/1288132283443142661
SWI-Prolog has an interesting solution to the catch/throw
problem. It offers two different catch:
- catch/3: Does not build a backtrace
- catch_with_backtrace/3: As the name says, builds a backtrace
We did something else in Jekejeke Prolog. We had two types
of internal Prolog errors:
- EngineMessage: Prolog error without backtrace
- EngineException: Prolog error with backtrace
This was less motivated by performance considerations, such
as number_codes/2 exceptions, but rather by the observation that
some code has access to Engine, and can therefore fetch
backtrace, and other code does not have an Engine parameter,
and EngineMessage would be thrown, and the backtrace would be
fetched later.
The EngineMessage and EngineException combo works
excellently internally in Java code. But when moving outside
of Java, into Prolog code, we decided to always convert
into an error with a backtrace. So inside Prolog code there
is no more benefit, and calling number_codes/2 inside Prolog
will not benefit. This is a little annoying for the Dogelog runtime
which aims at doing more stuff in Prolog itself. So there
is now a Dogelog runtime proposal, to have a backtrace, and
maybe even shamelessly adopt catch_with_backtrace/3:
Use spare wheel for backtrace in throw/1 #86 https://github.com/jburse/dogelog-moon/issues/86
Not yet sure. But its not yet clear how this proposal should work
out, if a catch/3 doesn't catch a ball, and hands it down to catch_with_backtrace/1. How can it add a backtrace after
the fact? Maybe the rethrow will only have a backtarce
to catch/3 and not its early history.
Mostowski Collapse schrieb am Mittwoch, 28. Juli 2021 um 11:19:53 UTC+2:
SWI-Prolog has an interesting solution to the catch/throw
problem. It offers two different catch:
- catch/3: Does not build a backtrace
- catch_with_backtrace/3: As the name says, builds a backtrace
We did something else in Jekejeke Prolog. We had two types
of internal Prolog errors:
- EngineMessage: Prolog error without backtrace
- EngineException: Prolog error with backtrace
This was less motivated by performance considerations, such
as number_codes/2 exceptions, but rather by the observation that
some code has access to Engine, and can therefore fetch
backtrace, and other code does not have an Engine parameter,
and EngineMessage would be thrown, and the backtrace would be
fetched later.
The SAT solver IsaSAT by Mathias Fleury has won the
fixed CNF encoding race of the 2021 EDA Challenge. All results.
IsaSAT is a formally verified SAT solver, using Peter Lammich's
Isabelle LLVM to produce fast verified code.
This is the first time a formally verified solver wins a competition
against unverified solvers.
http://fmv.jku.at/papers/Fleury-EDA-Challenge-2021.pdf
Interesting take on a verified SAT solver. They have two proofs.
One proof shows that the SAT solver is sound and complete
unconditionally. Such a proof needs to assume natural numbers,
which are then used to encode literals, clauses, etc.. From such
a proof one can extract code for an abstract machine that
has big numbers, that might nevertheless throw a resource
error when memory is exhaustet. Then they have a second proof
where they assume a more down to earth encoding of
literals, clauses, etc.. by assuming stuff is encoded in 64-bit
or somesuch. In such a proof there is not anymore completeness.
The SAT solver is already inheritenly incompletely viewed
on the verification level. Whats the advantage of such an approach?
Mostowski Collapse schrieb am Dienstag, 26. Oktober 2021 um 09:57:20 UTC+2:
The SAT solver IsaSAT by Mathias Fleury has won the
fixed CNF encoding race of the 2021 EDA Challenge. All results.
IsaSAT is a formally verified SAT solver, using Peter Lammich's
Isabelle LLVM to produce fast verified code.
This is the first time a formally verified solver wins a competition against unverified solvers.
http://fmv.jku.at/papers/Fleury-EDA-Challenge-2021.pdf
Now toying around with SWI-Prolog s(CASP). Wonder
why it has ASP = Answer Set Programming in its name?
https://swish.swi-prolog.org/p/scasp_constraint_tests.pl
I am trying this:
false :- not p, not q.
p :- p.
q :- q.
r :- p.
r :- q.
Shouldn’t the query ? r succeed? It gives me false.
Ok my bad, “not” is not classical negation, even clingo cant
do it. The clause false :- not p, not q would be logical equivalent
to p | q :- true if “not” were classical.
But then I have a disjunctive head. How enter a disjunctive
head in s(CASP)? In clingo I can do:
p | q.
p :- p.
q :- q.
r :- p.
r :- q.
And as expected it gives me two stable models.
Answer: 1
q r
Answer: 2
p r
But SWI-Prolog s(CASP) gives me nothing. Was comparing to:
https://potassco.org/clingo/run/
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
Now toying around with SWI-Prolog s(CASP). Wonder
why it has ASP = Answer Set Programming in its name?
https://swish.swi-prolog.org/p/scasp_constraint_tests.pl
I am trying this:
false :- not p, not q.
p :- p.
q :- q.
r :- p.
r :- q.
Shouldn’t the query ? r succeed? It gives me false.
So some conclusion was that s(CASP) probably doesn't
do disjunctive logic programming. The example we had
was as folllows:
:- abducible p, q.
false :- -p, -q.
r :- p, q.
https://swish.swi-prolog.org/p/disj_trial3.pl
From classical logic and also in ordinary ASP, we will
not find that r occurs in all stable models. On the
other hand s(CAPS) seems to be able
to prove both r and not r. LoL
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
Ok my bad, “not” is not classical negation, even clingo cant
do it. The clause false :- not p, not q would be logical equivalent
to p | q :- true if “not” were classical.
But then I have a disjunctive head. How enter a disjunctive
head in s(CASP)? In clingo I can do:
p | q.
p :- p.
q :- q.
r :- p.
r :- q.
And as expected it gives me two stable models.
Answer: 1
q r
Answer: 2
p r
But SWI-Prolog s(CASP) gives me nothing. Was comparing to:
https://potassco.org/clingo/run/
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
Now toying around with SWI-Prolog s(CASP). Wonder
why it has ASP = Answer Set Programming in its name?
https://swish.swi-prolog.org/p/scasp_constraint_tests.pl
I am trying this:
false :- not p, not q.
p :- p.
q :- q.
r :- p.
r :- q.
Shouldn’t the query ? r succeed? It gives me false.
Our own conclusion, that we can prove r and not r,
was that abduction is involved.
If P is the s(CASP) program, and A is what was abducted, then
the s(CASP) query Q is resolved against the program P and the
the abducted facts A. So that you have:
P, A |- Q.
When I asked r, it abducted p,q. When I asked not r, it abducted ~p.
What was abducted is seen in the s(CASP) model section.
For example for the abducible fact p, the _p makes ~p.
Oki Doki.
Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:49:25 UTC+1:
So some conclusion was that s(CASP) probably doesn't
do disjunctive logic programming. The example we had
was as folllows:
:- abducible p, q.
false :- -p, -q.
r :- p, q.
https://swish.swi-prolog.org/p/disj_trial3.pl
From classical logic and also in ordinary ASP, we will
not find that r occurs in all stable models. On the
other hand s(CAPS) seems to be able
to prove both r and not r. LoL
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
Ok my bad, “not” is not classical negation, even clingo cant
do it. The clause false :- not p, not q would be logical equivalent
to p | q :- true if “not” were classical.
But then I have a disjunctive head. How enter a disjunctive
head in s(CASP)? In clingo I can do:
p | q.
p :- p.
q :- q.
r :- p.
r :- q.
And as expected it gives me two stable models.
Answer: 1
q r
Answer: 2
p r
But SWI-Prolog s(CASP) gives me nothing. Was comparing to:
https://potassco.org/clingo/run/
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
Now toying around with SWI-Prolog s(CASP). Wonder
why it has ASP = Answer Set Programming in its name?
https://swish.swi-prolog.org/p/scasp_constraint_tests.pl
I am trying this:
false :- not p, not q.
p :- p.
q :- q.
r :- p.
r :- q.
Shouldn’t the query ? r succeed? It gives me false.
There is an interesting relationship to QSAT. Namely
we can do abduction in QSAT. At least it seems to me.
First look at deduction and not abduction. Deduction
would be verification of P |- Q, with P and Q given,
no abducible A involved. In QSAT we can ask:
/* SWI-Prolog */
?- sat(~(V^ ~(P =< Q))).
What does this all mean? Well V are the propositional
variables, and (^)/2 is the QSAT proositional existential
quantifier, (~)/1 is boolean negation and (=<)/2 is boolean
implication. So the problem I posed for ASP was simply:
P: The logic program:
p v q.
r <- p & q.
Q: The query to the logic program:
?- r.
Now with a QSAT solver, such as SWI-Prolog, we see that
r is not provable, namely we have:
?- use_module(library(clpb)).
true.
?- sat(~(P^Q^R^ ~((P+Q)*(R>=P*Q)=<R))).
false.
Cool!
Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:50:23 UTC+1:
Our own conclusion, that we can prove r and not r,
was that abduction is involved.
If P is the s(CASP) program, and A is what was abducted, then
the s(CASP) query Q is resolved against the program P and the
the abducted facts A. So that you have:
P, A |- Q.
When I asked r, it abducted p,q. When I asked not r, it abducted ~p.
What was abducted is seen in the s(CASP) model section.
For example for the abducible fact p, the _p makes ~p.
Oki Doki.
Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:49:25 UTC+1:
So some conclusion was that s(CASP) probably doesn't
do disjunctive logic programming. The example we had
was as folllows:
:- abducible p, q.
false :- -p, -q.
r :- p, q.
https://swish.swi-prolog.org/p/disj_trial3.pl
From classical logic and also in ordinary ASP, we will
not find that r occurs in all stable models. On the
other hand s(CAPS) seems to be able
to prove both r and not r. LoL
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
Ok my bad, “not” is not classical negation, even clingo cant
do it. The clause false :- not p, not q would be logical equivalent
to p | q :- true if “not” were classical.
But then I have a disjunctive head. How enter a disjunctive
head in s(CASP)? In clingo I can do:
p | q.
p :- p.
q :- q.
r :- p.
r :- q.
And as expected it gives me two stable models.
Answer: 1
q r
Answer: 2
p r
But SWI-Prolog s(CASP) gives me nothing. Was comparing to:
https://potassco.org/clingo/run/
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
Now toying around with SWI-Prolog s(CASP). Wonder
why it has ASP = Answer Set Programming in its name?
https://swish.swi-prolog.org/p/scasp_constraint_tests.pl
I am trying this:
false :- not p, not q.
p :- p.
q :- q.
r :- p.
r :- q.
Shouldn’t the query ? r succeed? It gives me false.
Now how do we do abduction. Well we split the propositonal
variables V into two camps, V1 the abducible ones, and V2
the normal ones. And then we issue the following question
towards the QSAT solver:
/* SWI-Prolog */
?- sat(V1 ~(V2^ ~(P =< Q))).
Lets do this for the example where r wasn't provable from
deduction alone. We make p and q abducible. Eh voila
r becomes provable:
?- sat(P^Q^ ~(R^ ~((P+Q)*(R>=P*Q)=<R))).
sat(P=:=P),
sat(Q=:=Q),
sat(R=:=R).
The sat(X=:=X) constraints can be ignored, they just say
that X is boolean. So this is now basically a true. We can also
ask ~r, and see that it also becomes provable:
?- sat(P^Q^ ~(R^ ~((P+Q)*(R>=P*Q)=< ~R))).
sat(P=:=P),
sat(Q=:=Q),
sat(R=:=R).
Thats pretty cool!
Mostowski Collapse schrieb am Samstag, 6. November 2021 um 20:07:33 UTC+1:
There is an interesting relationship to QSAT. Namely
we can do abduction in QSAT. At least it seems to me.
First look at deduction and not abduction. Deduction
would be verification of P |- Q, with P and Q given,
no abducible A involved. In QSAT we can ask:
/* SWI-Prolog */
?- sat(~(V^ ~(P =< Q))).
What does this all mean? Well V are the propositional
variables, and (^)/2 is the QSAT proositional existential
quantifier, (~)/1 is boolean negation and (=<)/2 is boolean
implication. So the problem I posed for ASP was simply:
P: The logic program:
p v q.
r <- p & q.
Q: The query to the logic program:
?- r.
Now with a QSAT solver, such as SWI-Prolog, we see that
r is not provable, namely we have:
?- use_module(library(clpb)).
true.
?- sat(~(P^Q^R^ ~((P+Q)*(R>=P*Q)=<R))).
false.
Cool!
Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:50:23 UTC+1:
Our own conclusion, that we can prove r and not r,
was that abduction is involved.
If P is the s(CASP) program, and A is what was abducted, then
the s(CASP) query Q is resolved against the program P and the
the abducted facts A. So that you have:
P, A |- Q.
When I asked r, it abducted p,q. When I asked not r, it abducted ~p. What was abducted is seen in the s(CASP) model section.
For example for the abducible fact p, the _p makes ~p.
Oki Doki.
Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:49:25 UTC+1:
So some conclusion was that s(CASP) probably doesn't
do disjunctive logic programming. The example we had
was as folllows:
:- abducible p, q.
false :- -p, -q.
r :- p, q.
https://swish.swi-prolog.org/p/disj_trial3.pl
From classical logic and also in ordinary ASP, we will
not find that r occurs in all stable models. On the
other hand s(CAPS) seems to be able
to prove both r and not r. LoL
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
Ok my bad, “not” is not classical negation, even clingo cant
do it. The clause false :- not p, not q would be logical equivalent to p | q :- true if “not” were classical.
But then I have a disjunctive head. How enter a disjunctive
head in s(CASP)? In clingo I can do:
p | q.
p :- p.
q :- q.
r :- p.
r :- q.
And as expected it gives me two stable models.
Answer: 1
q r
Answer: 2
p r
But SWI-Prolog s(CASP) gives me nothing. Was comparing to:
https://potassco.org/clingo/run/
Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
Now toying around with SWI-Prolog s(CASP). Wonder
why it has ASP = Answer Set Programming in its name?
https://swish.swi-prolog.org/p/scasp_constraint_tests.pl
I am trying this:
false :- not p, not q.
p :- p.
q :- q.
r :- p.
r :- q.
Shouldn’t the query ? r succeed? It gives me false.
Was toying around with proof by cases, two versions
here of the Yale shooting problem:
/* s(CAPS) Style */
https://swish.swi-prolog.org/p/yale_shooting.pl
/* Negation as Failure Style */ https://swish.swi-prolog.org/p/yale_shooting2.pl
Had to double check, wasn’t sure anymore about my
claims. Could be that I am already rusty. Yes if you add
proof by cases to intuitionistic logic, you get classical logic.
At last Wikipedia also says so:
The system of classical logic is obtained by adding any one of the following axioms:
ϕ ∨ ¬ ϕ (Law of the excluded middle.
May also be formulated as ( ϕ → χ ) → ( ( ¬ ϕ → χ ) → χ ).)
https://en.wikipedia.org/wiki/Intuitionistic_logic#Relation_to_classical_logic
Now (A → (B → C)) is the same as A & B → C, so an alternative
to the Law of excluded middle (LEM) is indeed proof by cases.
I tried this one now with s(CASP):
p(X,X).
q(X,Y) :- not p(X,Y).
?- ? q(X,Y).
And it gives me false. I was expecting dif(X,Y) instead.
Or what is the C in s(CASP)? C stands for constraints, right?
Edit 16.11.2021:
The original constructive negation paper (David Chan. 1988.
Constructive negation based on the completed database. In Proc. of ICLP-88.) would at least require such an answer, since the completion of the fact p(X,X) is:
p(X,Y) <-> X = Y.
So when I call not p(X,Y), I basically call not X = Y, and the negation of unification
would be dif(X,Y) or somesuch. Can be expressed as constraint. The example simple and doesn’t require quantifier elimination.
MiniKanren has recently tried to handle quantifiers:
Constructive Negation for MiniKanren http://minikanren.org/workshop/2019/minikanren19-final4.pdf
This shows me that functional programming is on the decline:
Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
I wonder whether this will have an impact on proof assistants.
Some of them have clearly a functional programming inclining.
This is also an interesting article, mentioning a new
trend such as "Multiparadigm languages":
Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
We just observed that Python 3.10 introduced a new
pattern matching construct. Now there is a proposal
for Java JDK 17 followup for some pattern matching
like switch statement. I guess there is an unspoken law:
"Every programming language over the long
run will evolve into some Prolog variant"
Well this is too harsh, maybe this pattern matching only
mimicks Haskell single sided unification and not Prolog
unification. But what if people get fed up
with single sided unification?
LoL
Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
This shows me that functional programming is on the decline:
Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
I wonder whether this will have an impact on proof assistants.
Some of them have clearly a functional programming inclining.
There was a proposal: https://area51.stackexchange.com/proposals/29144/beginner-theoretical-computer-science
But it now says:
This proposal has been deleted
Now if you want to join cstheory.stackexchange.com it
says Anybody can ask a question Anybody can answer
The best answers are voted up and rise to the top
But if you do that, they slap their policy into your face:
It allows only questions that "can be discussed between
two professors or between two graduate students working
on Ph.D.'s, but not usually between a professor and a
typical undergraduate student". https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed
I am not lying when I say even Andrej Bauer did
that. But how do you want to launch a proof assistants
site, I assume for everybody? if you cannot divert
cs theory questions to another stackexchange?
proof assistants are full of cs theory stuff.
Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
Maybe the assumption that programming language further
evolve is wrong, they could also devolve to assembler again?
Awaken In 2505, Humans Devolve
https://www.youtube.com/watch?v=mnLxc954ipo
At least this would truely help to have full control of
the performance and memory allocation of your code.
LMAO!
Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
This is also an interesting article, mentioning a new
trend such as "Multiparadigm languages":
Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
We just observed that Python 3.10 introduced a new
pattern matching construct. Now there is a proposal
for Java JDK 17 followup for some pattern matching
like switch statement. I guess there is an unspoken law:
"Every programming language over the long
run will evolve into some Prolog variant"
Well this is too harsh, maybe this pattern matching only
mimicks Haskell single sided unification and not Prolog
unification. But what if people get fed up
with single sided unification?
LoL
Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
This shows me that functional programming is on the decline:
Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
I wonder whether this will have an impact on proof assistants.
Some of them have clearly a functional programming inclining.
Maybe the assumption that programming language further
evolve is wrong, they could also devolve to assembler again?
Awaken In 2505, Humans Devolve
https://www.youtube.com/watch?v=mnLxc954ipo
At least this would truely help to have full control of
the performance and memory allocation of your code.
LMAO!
Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
This is also an interesting article, mentioning a new
trend such as "Multiparadigm languages":
Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
We just observed that Python 3.10 introduced a new
pattern matching construct. Now there is a proposal
for Java JDK 17 followup for some pattern matching
like switch statement. I guess there is an unspoken law:
"Every programming language over the long
run will evolve into some Prolog variant"
Well this is too harsh, maybe this pattern matching only
mimicks Haskell single sided unification and not Prolog
unification. But what if people get fed up
with single sided unification?
LoL
Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
This shows me that functional programming is on the decline:
Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
I wonder whether this will have an impact on proof assistants.
Some of them have clearly a functional programming inclining.
Maybe the assumption that programming language further
evolve is wrong, they could also devolve to assembler again?
Awaken In 2505, Humans Devolve
https://www.youtube.com/watch?v=mnLxc954ipo
At least this would truely help to have full control of
the performance and memory allocation of your code.
LMAO!
Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
This is also an interesting article, mentioning a new
trend such as "Multiparadigm languages":
Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/
We just observed that Python 3.10 introduced a new
pattern matching construct. Now there is a proposal
for Java JDK 17 followup for some pattern matching
like switch statement. I guess there is an unspoken law:
"Every programming language over the long
run will evolve into some Prolog variant"
Well this is too harsh, maybe this pattern matching only
mimicks Haskell single sided unification and not Prolog
unification. But what if people get fed up
with single sided unification?
LoL
Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
This shows me that functional programming is on the decline:
Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming
I wonder whether this will have an impact on proof assistants.
Some of them have clearly a functional programming inclining.
Interesting call:
"For example, have a look at the Coq standard libarary or
the user contributions, these are formalizations of
mathematics in type theory. And this stuff is written mostly
by computer scientists. If mathematicians moved onto
the proof-assistant bandwagon, there would be much more." https://mathoverflow.net/a/133599
Maybe they would join the bandwagon if there were
less typos? Whats a "libarary"? Is it library? Or libarray?
LoL
To handle FOL matrices, unify_with_occurs_check/2 might
also come into play. Whats a short example and short
explanation about things that can go wrong?
Mostowski Collapse schrieb:
Small bug in the LK code:
There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
https://www.philipzucker.com/javascript-automated-proving/
Its not complete for FOL matrices, try this:
prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
Failed To Prove.
Now remove the cut in the axiom rule:
prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
X = s
Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
Interesting call:
"For example, have a look at the Coq standard libarary or
the user contributions, these are formalizations of
mathematics in type theory. And this stuff is written mostly
by computer scientists. If mathematicians moved onto
the proof-assistant bandwagon, there would be much more."
https://mathoverflow.net/a/133599
Maybe they would join the bandwagon if there were
less typos? Whats a "libarary"? Is it library? Or libarray?
LoL
Small bug in the LK code:
There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
https://www.philipzucker.com/javascript-automated-proving/
Its not complete for FOL matrices, try this:
prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
Failed To Prove.
Now remove the cut in the axiom rule:
prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
X = s
Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
Interesting call:
"For example, have a look at the Coq standard libarary or
the user contributions, these are formalizations of
mathematics in type theory. And this stuff is written mostly
by computer scientists. If mathematicians moved onto
the proof-assistant bandwagon, there would be much more."
https://mathoverflow.net/a/133599
Maybe they would join the bandwagon if there were
less typos? Whats a "libarary"? Is it library? Or libarray?
LoL
Oh, this is very nice!
On Thursday, 30 December 2021 at 10:06:49 UTC+1, burs...@gmail.com wrote:
Oh, this is very nice!There is nothing nice about a fucking retard and piece of spamming
shit polluting all public ponds, you shameless retarded piece of shit.
But all I'd still want to know is who's the criminal nazi cunts who pay your bills...
*Plonk*
Julio
Lean TAP can be fun. Spent the whole day to
render MathJax. Then was annoyed by MathJax,
how do you put this thingy into an email?
So here is barber paradox in list form with Unicode:
1. s(a,a) ⊢ s(a,a) (ax)
2. s(a,a) ⊢ ∃zs(z,z) (R∃)
3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
4. s(a,a) ⊢ s(a,a) (ax)
5. s(a,a) ⊢ ∃zs(z,z) (R∃)
6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html
So how was it done? First one needs to reduce proof noise:
Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785
Dogelog Player removes proof noise
https://www.facebook.com/groups/dogelog
Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
Lean TAP can be fun. Spent the whole day to
render MathJax. Then was annoyed by MathJax,
how do you put this thingy into an email?
So here is barber paradox in list form with Unicode:
1. s(a,a) ⊢ s(a,a) (ax)
2. s(a,a) ⊢ ∃zs(z,z) (R∃)
3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
4. s(a,a) ⊢ s(a,a) (ax)
5. s(a,a) ⊢ ∃zs(z,z) (R∃)
6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html
Oki Doki, full first order logic can be also rendered now:
Leibniz’s Dream in Dogelog Player https://twitter.com/dogelogch/status/1477779371628933121
Leibniz’s Dream in Dogelog Player
https://www.facebook.com/groups/dogelog
Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
So how was it done? First one needs to reduce proof noise:
Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785
Dogelog Player removes proof noise
https://www.facebook.com/groups/dogelog
Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
Lean TAP can be fun. Spent the whole day to
render MathJax. Then was annoyed by MathJax,
how do you put this thingy into an email?
So here is barber paradox in list form with Unicode:
1. s(a,a) ⊢ s(a,a) (ax)
2. s(a,a) ⊢ ∃zs(z,z) (R∃)
3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
4. s(a,a) ⊢ s(a,a) (ax)
5. s(a,a) ⊢ ∃zs(z,z) (R∃)
6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html
I am afraid, I didn't post the full Barber Paradox. I only posted
what was found in Jens Ottens ex_barber.pl. Now a regret not
providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber
paradox cannot so concisely be formulate without (<=>)/2.
What would be fun is not only XOR-SAT but also XOR-FOL.
The Jens Otten provers can solve FOL problems among which
we also find FOL problems in prenex normal form Q1x1…QnxnM
where Q1,…,Qn are the alternating quantifier blocks and M is
the FOL matrix. Quantifiers are handled in Jens Otten provers:
Qj=∀: is handled by a Skolem function.
Qj=∃: is handled by fresh variable and contraction.
Besides that all the 3 provers he presents, leanseq_v5.pl,
leantap_pure.pl and leancop_pure.pl do the same with the
FOL matrix M, they put it into conjunctive normal form (CNF),
and try to solve it via unification. Lets take the Barber Paradox
and see how the CNF looks like. The Barber Paradox with (<=>)/2:
¬∃x∀y(¬s(y,y) <=> s(x,y))
The Barber Paradox in prenex with CNF:
∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))
When the above is solved unification wise the same thing
happens twice for both conjuncts. But since the XOR-SAT
rewriting prototype has simp(A=A, 1) does this mean we could
solve XOR-FOL differently and for example have a FOL matrix
format where we solve P<=>Q by directly trying to unify P and Q?
Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
Oki Doki, full first order logic can be also rendered now:
Leibniz’s Dream in Dogelog Player https://twitter.com/dogelogch/status/1477779371628933121
Leibniz’s Dream in Dogelog Player https://www.facebook.com/groups/dogelog
Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
So how was it done? First one needs to reduce proof noise:
Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785
Dogelog Player removes proof noise https://www.facebook.com/groups/dogelog
Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
Lean TAP can be fun. Spent the whole day to
render MathJax. Then was annoyed by MathJax,
how do you put this thingy into an email?
So here is barber paradox in list form with Unicode:
1. s(a,a) ⊢ s(a,a) (ax)
2. s(a,a) ⊢ ∃zs(z,z) (R∃)
3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
4. s(a,a) ⊢ s(a,a) (ax)
5. s(a,a) ⊢ ∃zs(z,z) (R∃)
6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html
Nice! Now the example runs also from within Python. Even
on ordinary CMD on Windows 10. Just use for example this
font *NSimSum*, select it in the console properties.
See also:
Unicode Proof Listing in Dogelog Player https://twitter.com/dogelogch/status/1478315286491287553
Unicode Proof Listing in Dogelog Player https://www.facebook.com/groups/dogelog
But I have to simplify the Python Dogelog Player console.
Now the Python Dogelog Player console is a tutorial example,
but dogelog.py should do it by default.
Please be patient.
Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 11:49:53 UTC+1:
I am afraid, I didn't post the full Barber Paradox. I only posted
what was found in Jens Ottens ex_barber.pl. Now a regret not
providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber
paradox cannot so concisely be formulate without (<=>)/2.
What would be fun is not only XOR-SAT but also XOR-FOL.
The Jens Otten provers can solve FOL problems among which
we also find FOL problems in prenex normal form Q1x1…QnxnM
where Q1,…,Qn are the alternating quantifier blocks and M is
the FOL matrix. Quantifiers are handled in Jens Otten provers:
Qj=∀: is handled by a Skolem function.
Qj=∃: is handled by fresh variable and contraction.
Besides that all the 3 provers he presents, leanseq_v5.pl,
leantap_pure.pl and leancop_pure.pl do the same with the
FOL matrix M, they put it into conjunctive normal form (CNF),
and try to solve it via unification. Lets take the Barber Paradox
and see how the CNF looks like. The Barber Paradox with (<=>)/2:
¬∃x∀y(¬s(y,y) <=> s(x,y))
The Barber Paradox in prenex with CNF:
∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))
When the above is solved unification wise the same thing
happens twice for both conjuncts. But since the XOR-SAT
rewriting prototype has simp(A=A, 1) does this mean we could
solve XOR-FOL differently and for example have a FOL matrix
format where we solve P<=>Q by directly trying to unify P and Q?
Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
Oki Doki, full first order logic can be also rendered now:
Leibniz’s Dream in Dogelog Player https://twitter.com/dogelogch/status/1477779371628933121
Leibniz’s Dream in Dogelog Player https://www.facebook.com/groups/dogelog
Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
So how was it done? First one needs to reduce proof noise:
Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785
Dogelog Player removes proof noise https://www.facebook.com/groups/dogelog
Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
Lean TAP can be fun. Spent the whole day to
render MathJax. Then was annoyed by MathJax,
how do you put this thingy into an email?
So here is barber paradox in list form with Unicode:
1. s(a,a) ⊢ s(a,a) (ax)
2. s(a,a) ⊢ ∃zs(z,z) (R∃)
3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
4. s(a,a) ⊢ s(a,a) (ax)
5. s(a,a) ⊢ ∃zs(z,z) (R∃)
6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)
http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html
Now having more fun with Jens Ottens Lean Prover. This
is a nice little example, where 1 contraction doesn’t work,
but 2 contractions work:
?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
fail.
?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
true.
See also:
Maslovs Method in Dogelog Player https://twitter.com/dogelogch/status/1479792480908414979
Maslovs Method in Dogelog Player
https://www.facebook.com/groups/dogelog
One more iteration of our prover:
Proof systems that are based on the Howard-Curry isomorphism
and that extract proof terms in the lambda calculus are familiar
to node dropping. Lambda calculus expressions have a notion
of variable occurence.
/* Eta Reduction */
λx(Mx) ~~> M for x ∉ M
Variable occurence can then be used similarly to has_usage/2
to shorten proof terms in the form of lambda expressions. A
prominent reduction rule is seen in the above that goes by
the name eta reduction.
Our provers do extract terms where we store integer sequent
indexes of used formulas. For the newest variant we generalized
the terms to alfa, beta, gamma and delta, but we currently do
not use a generic binder format.
See also:
Node Dropping for Maslovs Method https://twitter.com/dogelogch/status/1480091985222451201
Node Dropping for Maslovs Method
https://www.facebook.com/groups/dogelog
Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 16:57:45 UTC+1:
The problem with the French logician is, that he does not
get through the thicket of classical logic into the Maslovs method.
He only shows a translation for intuitionstic logic in the following form:
(∃xA)* := ∃x !A
https://girard.perso.math.cnrs.fr/Synsem.pdf
Given his other definitions for other connectives and quantifiers
it might work. In his “Table 2: Classical connectives : definition in terms of linear logic” he then repeats this translation.
I think his translation works since he has exponentation
elsewhere outside of the quantifier. But the Maslov method shows
that the outside exponentation in classical connectives is
superflous, and that we can put the exponentiation in front
of a certain quantifier.
Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
Now having more fun with Jens Ottens Lean Prover. This
is a nice little example, where 1 contraction doesn’t work,
but 2 contractions work:
?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
fail.
?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
true.
See also:
Maslovs Method in Dogelog Player https://twitter.com/dogelogch/status/1479792480908414979
Maslovs Method in Dogelog Player
https://www.facebook.com/groups/dogelog
The problem with the French logician is, that he does not
get through the thicket of classical logic into the Maslovs method.
He only shows a translation for intuitionstic logic in the following form:
(∃xA)* := ∃x !A
https://girard.perso.math.cnrs.fr/Synsem.pdf
Given his other definitions for other connectives and quantifiers
it might work. In his “Table 2: Classical connectives : definition in terms of linear logic” he then repeats this translation.
I think his translation works since he has exponentation
elsewhere outside of the quantifier. But the Maslov method shows
that the outside exponentation in classical connectives is
superflous, and that we can put the exponentiation in front
of a certain quantifier.
Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
Now having more fun with Jens Ottens Lean Prover. This
is a nice little example, where 1 contraction doesn’t work,
but 2 contractions work:
?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
fail.
?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
true.
See also:
Maslovs Method in Dogelog Player https://twitter.com/dogelogch/status/1479792480908414979
Maslovs Method in Dogelog Player
https://www.facebook.com/groups/dogelog
I did the barber paradox always wrong!
The biconditional makes it so much easier.
1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
5. ¬¬s(a, a) (F∧2 4)
6. ¬s(a, a) (F∧1 4)
7. s(a, a) (F¬ 5)
✓ (ax 6, 7)
4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
5. ¬s(a, a) (T∨2 4)
6. s(a, a) (T∨1 4)
✓ (ax 5, 6)
See also:
Biconditional Support for Maslovs Method https://twitter.com/dogelogch/status/1483455561031106563
Biconditional Support for Maslovs Method https://www.facebook.com/groups/dogelog
Its a pitty that there is no simple leanTap=, i.e. leanTap= with
equality. My take is only a few lines, splitting (subst) into (subst1)
and (subst2) and can run in the browser.
On the other hand I read:
The completion-based method for mixed E-unification we
have described, has been implemented as part of the
tableau-based theorem prover 3TAP [3]. The implementation
consists of about 2500 lines of code, written in Quintus Prolog.
Besides the possibility to prove theorems from predicate logic
with equality, the E-unification module can be used “stand alone”
to solve simultaneous mixed E-unification problems. https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf
I don’t know how to run 2500 lines of code in the browser.
And I don’t need some first order equality that would even
deploy some term order, as is popular in certain term
rewriting and Knuth Bendix. One interesting test case is this
one, that works in the browser:
?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\ f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
% Wall 60 ms, gc 0 ms, 1171000 lips
Thanks to McCarthys trick its quite fast. On monday it still took
me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz
tool can do the same, but interestingly he gets a longer proof with
more (subst) applications. See also this ticket:
Does the tree tool search shortest proofs? #11 https://github.com/wo/tpg/issues/11
Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 16:57:38 UTC+1:
I did the barber paradox always wrong!
The biconditional makes it so much easier.
1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
5. ¬¬s(a, a) (F∧2 4)
6. ¬s(a, a) (F∧1 4)
7. s(a, a) (F¬ 5)
✓ (ax 6, 7)
4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
5. ¬s(a, a) (T∨2 4)
6. s(a, a) (T∨1 4)
✓ (ax 5, 6)
See also:
Biconditional Support for Maslovs Method https://twitter.com/dogelogch/status/1483455561031106563
Biconditional Support for Maslovs Method https://www.facebook.com/groups/dogelog
See also my blog post on medium.com:
McCarthys Trick for First Order Equality https://twitter.com/dogelogch/status/1484032442717585409
McCarthys Trick for First Order Equality https://www.facebook.com/groups/dogelog
Here is a poket McCarthy for propositional logic only.
It can also do Joseph Vidal-Rossets antisequent (asq):
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
prove(G>[~A,B|D],P).
prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
prove(G>[A,B|D],P).
/* double negation */
prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
prove(G>[A|D],P).
prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
prove(G>[~A,~B|D],P).
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
prove(G>[~A,~B|D],P1),
prove(G>[A,B|D],P2).
prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[~B|D],P2).
prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[B|D],P2).
prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
prove(G>[~A|D],P1),
prove(G>[~B|D],P2).
prove(G>[A|D], ax(G>[A|D], A)):-
member(B,G), A==B, !.
/* next */
prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
prove([A|G]>D,P).
prove(G>[A|D], lneg(G>[A|D], P)) :- !,
prove([~A|G]>D,P).
prove(G>[], asq(G>[], asq)).
provable(F,P):-
prove([]>[F],P).
member(E, [E|_]).
member(E, [_|Xs]) :-
member(E, Xs).
Why does Jens Otten automatic reordering preprocessing
give some bang? Now I get for Pelletier problem 71:
/* Joseph Vidal-Rossets LeanSeq, from his web site */
?- test.
% 54,202,362 inferences, 4.969 CPU in 5.017 seconds
(99% CPU, 10908954 Lips)
true. https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html
/* My McCarthy */
?- test2.
% 8,814,592 inferences, 1.099 CPU in 1.123 seconds
(98% CPU, 8019776 Lips)
true.
I think this is because rbicond is more symmetric,
in my new McCarthy it is now:
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
On the other hand Joseph Vidal-Rossets LeanSeq
has the following rbicond rule:
prove(G>D, rbicond(G>D,P1,P2)):-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],P1),
prove([B|G]>[A|D1], P2).
But this works only for Pelletier problem 71.
The rule is still quite static, and doesn't
do any reordering.
Mostowski Collapse schrieb:
Here is a poket McCarthy for propositional logic only.
It can also do Joseph Vidal-Rossets antisequent (asq):
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
prove(G>[~A,B|D],P).
prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
prove(G>[A,B|D],P).
/* double negation */
prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
prove(G>[A|D],P).
prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
prove(G>[~A,~B|D],P).
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
prove(G>[~A,~B|D],P1),
prove(G>[A,B|D],P2).
prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[~B|D],P2).
prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[B|D],P2).
prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
prove(G>[~A|D],P1),
prove(G>[~B|D],P2).
prove(G>[A|D], ax(G>[A|D], A)):-
member(B,G), A==B, !.
/* next */
prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
prove([A|G]>D,P).
prove(G>[A|D], lneg(G>[A|D], P)) :- !,
prove([~A|G]>D,P).
prove(G>[], asq(G>[], asq)).
provable(F,P):-
prove([]>[F],P).
member(E, [E|_]).
member(E, [_|Xs]) :-
member(E, Xs).
There is a bug in nff_pure.pl by Jens Otten. This here:
Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,
Should read, so that it runs in a wider variety of Prolog systems:
Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,
And we can now try Pelletier problem 71, and it doesn’t work:
% 88,652,639 inferences, 13.734 CPU in 13.999 seconds
(98% CPU, 6454800 Lips)
ERROR: Stack limit (1.0Gb) exceeded
Strange...
Mostowski Collapse schrieb:
Why does Jens Otten automatic reordering preprocessing
give some bang? Now I get for Pelletier problem 71:
/* Joseph Vidal-Rossets LeanSeq, from his web site */
?- test.
% 54,202,362 inferences, 4.969 CPU in 5.017 seconds
(99% CPU, 10908954 Lips)
true. https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html
/* My McCarthy */
?- test2.
% 8,814,592 inferences, 1.099 CPU in 1.123 seconds
(98% CPU, 8019776 Lips)
true.
I think this is because rbicond is more symmetric,
in my new McCarthy it is now:
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
On the other hand Joseph Vidal-Rossets LeanSeq
has the following rbicond rule:
prove(G>D, rbicond(G>D,P1,P2)):-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],P1),
prove([B|G]>[A|D1], P2).
But this works only for Pelletier problem 71.
The rule is still quite static, and doesn't
do any reordering.
Mostowski Collapse schrieb:
Here is a poket McCarthy for propositional logic only.
It can also do Joseph Vidal-Rossets antisequent (asq):
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
prove(G>[~A,B|D],P).
prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
prove(G>[A,B|D],P).
/* double negation */
prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
prove(G>[A|D],P).
prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
prove(G>[~A,~B|D],P).
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
prove(G>[~A,~B|D],P1),
prove(G>[A,B|D],P2).
prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[~B|D],P2).
prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[B|D],P2).
prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
prove(G>[~A|D],P1),
prove(G>[~B|D],P2).
prove(G>[A|D], ax(G>[A|D], A)):-
member(B,G), A==B, !.
/* next */
prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
prove([A|G]>D,P).
prove(G>[A|D], lneg(G>[A|D], P)) :- !,
prove([~A|G]>D,P).
prove(G>[], asq(G>[], asq)).
provable(F,P):-
prove([]>[F],P).
member(E, [E|_]).
member(E, [_|Xs]) :-
member(E, Xs).
The completion-based method for mixed E-unification we
have described, has been implemented as part of the
tableau-based theorem prover 3TAP [3]. The implementation
consists of about 2500 lines of code, written in Quintus Prolog.
Besides the possibility to prove theorems from predicate logic
with equality, the E-unification module can be used “stand alone”
to solve simultaneous mixed E-unification problems. https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf
If I paste my poket McCarthy into Joseph Vidal-Rossets web
page, I can reproduce the example from page 7 of this paper:
leanTAP Revisited
Melvin Fitting - March 13, 1997 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf
Simply use this here:
?- provable(((~p & q) | p), Proof).
The red color shows where the proof tree ends in Γ |- .
Joseph Vidal-Rosset could make a fork of his website,
that provides poket McCarthy directly for experimentation,
also using better proof tree lables. My own web site
does not yet show some red color. Thats a little too
early. First need to get my head around model finding
from tableaux for the non-propositional case...
Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 01:32:19 UTC+1:
There is a bug in nff_pure.pl by Jens Otten. This here:
Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,
Should read, so that it runs in a wider variety of Prolog systems:
Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,
And we can now try Pelletier problem 71, and it doesn’t work:
% 88,652,639 inferences, 13.734 CPU in 13.999 seconds
(98% CPU, 6454800 Lips)
ERROR: Stack limit (1.0Gb) exceeded
Strange...
Mostowski Collapse schrieb:
Why does Jens Otten automatic reordering preprocessing
give some bang? Now I get for Pelletier problem 71:
/* Joseph Vidal-Rossets LeanSeq, from his web site */
?- test.
% 54,202,362 inferences, 4.969 CPU in 5.017 seconds
(99% CPU, 10908954 Lips)
true. https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html
/* My McCarthy */
?- test2.
% 8,814,592 inferences, 1.099 CPU in 1.123 seconds
(98% CPU, 8019776 Lips)
true.
I think this is because rbicond is more symmetric,
in my new McCarthy it is now:
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !, prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
On the other hand Joseph Vidal-Rossets LeanSeq
has the following rbicond rule:
prove(G>D, rbicond(G>D,P1,P2)):-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],P1),
prove([B|G]>[A|D1], P2).
But this works only for Pelletier problem 71.
The rule is still quite static, and doesn't
do any reordering.
Mostowski Collapse schrieb:
Here is a poket McCarthy for propositional logic only.
It can also do Joseph Vidal-Rossets antisequent (asq):
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, '|'). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
prove(G>[~A,B|D],P).
prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
prove(G>[A,B|D],P).
/* double negation */
prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
prove(G>[A|D],P).
prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
prove(G>[~A,~B|D],P).
prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
prove(G>[~A,B|D],P1),
prove(G>[A,~B|D], P2).
prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
prove(G>[~A,~B|D],P1),
prove(G>[A,B|D],P2).
prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[~B|D],P2).
prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
prove(G>[A|D],P1),
prove(G>[B|D],P2).
prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
prove(G>[~A|D],P1),
prove(G>[~B|D],P2).
prove(G>[A|D], ax(G>[A|D], A)):-
member(B,G), A==B, !.
/* next */
prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
prove([A|G]>D,P).
prove(G>[A|D], lneg(G>[A|D], P)) :- !,
prove([~A|G]>D,P).
prove(G>[], asq(G>[], asq)).
provable(F,P):-
prove([]>[F],P).
member(E, [E|_]).
member(E, [_|Xs]) :-
member(E, Xs).
Today a little show of what can go wrong: Question
was why does Jens Otten leanseq_v5.pl use this:
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
And not this:
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
The offending test case is this here:
∀y∃xFxy → ∃z∀tFzt is invalid.
Countermodel:
Domain: { 0, 1 }
F: { (0,0), (1,1) }
https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt
I guess there is some literature that explains everything. On the
other hand some Prolog experimentation could maybe help
increase intuition. leanseq_v5.pl first, and I get, limiting the
depth to 10, it already takes quite some time with 10 in this
automated prover which doesn’t have much optimizations:
% leanseq_v5.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
iteration 3
iteration 4
iteration 5
iteration 6
iteration 7
iteration 8
iteration 9
iteration 10
false.
Now the faulty leanseq_v5f.pl, where the Skolem function
is replaced by only a Skolem constant:
% leanseq_v5f.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
true
Mostowski Collapse schrieb am Sonntag, 30. Januar 2022 um 21:11:01 UTC+1:
Today a little show of what can go wrong: Question
was why does Jens Otten leanseq_v5.pl use this:
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
And not this:
prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K).
The offending test case is this here:
∀y∃xFxy → ∃z∀tFzt is invalid.
Countermodel:
Domain: { 0, 1 }
F: { (0,0), (1,1) }
https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt
Now I have obtained a new result, leanTap is not really needed,
leanSeq could also do? I was using negation normal form with leanSeq,
and now leanSeq is also extremly fast. Maybe because of some indexing?
I used a leanSeq variant that saturates the literals before it tries the quantifier.
When I compare the two, there is not anymore much difference between leanSeq and leanTap. Only the new leanSeq would allow easy proof extraction:
/* leanTap */
?- time((between(1,100,_), test(time), fail; true)).
% 3,011,100 inferences, 0.203 CPU in 0.206 seconds (99% CPU, 14823877 Lips) true.
/* leanSeq+NNF+literal saturation */
?- time((between(1,100,_), test(time), fail; true)).
% 8,858,800 inferences, 0.844 CPU in 0.853 seconds (99% CPU, 10499319 Lips) true.
The difference is only a factor of ca. 4. Not that bad. I used a simple negation normal form without any reordering for both.
Mostowski Collapse schrieb am Dienstag, 8. Februar 2022 um 12:28:05 UTC+1:
You can run leanTap in Dogelog player in the browser. For the
simple problems among Pelletier 17-46 I get the following
results (100 iterations, browser was Chrome no async/await):
System Time
Tau Prolog 323’000
Dogelog Player 2’441
Formerly Jekejeke 811
SWI 299
Will post a link to a fork later. I want to compare different normal forms, but still struggling with optimal way to compute prenex and mini-scope. Too large design space, so slow progress.
The simple problems are:
17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44
You can run leanTap in Dogelog player in the browser. For the
simple problems among Pelletier 17-46 I get the following
results (100 iterations, browser was Chrome no async/await):
System Time
Tau Prolog 323’000
Dogelog Player 2’441
Formerly Jekejeke 811
SWI 299
Will post a link to a fork later. I want to compare different normal
forms, but still struggling with optimal way to compute prenex and mini-scope. Too large design space, so slow progress.
The simple problems are:
17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44
Happy Birthday Jacques Herbrand
February 12th, 1908: French mathematician, worked in
math. logic and field theory, Jacques Herbrand, was born. https://twitter.com/sc_k/status/9011037015
Lectures on Jacques Herbrand as a Logician
https://arxiv.org/abs/0902.4682
with axes after having started a fire. But Tinguely’s next two self- destroying machines, entitled “Study for an End of the World,” performed more successfully, detonating themselves with considerable https://www.britannica.com/biography/Jean-Tinguely#ref290920
Probably something that would make Alain
Colmerauer happy. By way of EricGT on
SWI-Prolog discourse:
"Prolog broke into the top 20 again a few months ago
(should have captured it then for historical use).
As of June 2022 it is still at 20."
https://www.tiobe.com/tiobe-index/
I guess we can overtake Ruby, which is on 19,
if we provide some "Prolog on Rails". Anybody up to it?
Mostowski Collapse schrieb am Samstag, 9. Juli 2022 um 10:12:37 UTC+2:
Probably something that would make Alain
Colmerauer happy. By way of EricGT on
SWI-Prolog discourse:
"Prolog broke into the top 20 again a few months ago
(should have captured it then for historical use).
As of June 2022 it is still at 20."
https://www.tiobe.com/tiobe-index/
You can learn a lot from this animal, for example:
- Rule 1 of speedy exit:
for maximum speed, washing machine trophy, just drop it.
- Rule 2 of speedy exit:
same holds for tank, ammunition, riffle, etc.. etc..
Mostowski Collapse schrieb am Mittwoch, 14. September 2022 um 18:21:08 UTC+2:
Biologicians have found a new animal, speedy exit saurus
aka ruZZian soldier, its the fastest animal on this planet:
The fastest animals in the world... https://twitter.com/Igor_from_Kyiv_/status/1569758364783054849
Biologicians have found a new animal, speedy exit saurus
aka ruZZian soldier, its the fastest animal on this planet:
The fastest animals in the world... https://twitter.com/Igor_from_Kyiv_/status/1569758364783054849
I think probabilistic reasoning itself is borken
Somebody said:
I think probabilistic reasoning itself is borken
Well I was a purist like that also in the past. And I am still a
kind of purist like that in the present, avoiding probability
whenever possible. But its a nice little
mathematical model, which you can map to constraint logic
programming CLP(R). So if for example you have an
equation involving probability:
P(A & B) < P(C)
Then this says nothing else than the CLP(R) constraint:
w + z < z + y + x + c
Interesting replacement of setup_call_cleanup/3:
open(Path, read, Input),
catch(read_term(Input, Term, Options), Error,
(close(Input),throw(Error))),
close(Input) https://github.com/LogtalkDotOrg/logtalk3/blob/master/library/term_io/term_io.lgt
Can we use this for something?
Here is some testing, with dry implementation of the bag:
/* SWI-Prolog 9.1.4 */
/* N215 Solution */
?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
% 7,000,000 inferences, 0.875 CPU in 0.871 seconds (100% CPU, 8000000 Lips) true.
/* Logtalk Idiom */
?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
% 6,000,000 inferences, 0.500 CPU in 0.497 seconds (101% CPU, 12000000 Lips) true.
Scryer Prolog isn't that lucky. Their setup_call_cleanup/3
has some meta predicate issue. And their catch/3 is utterly slow.
/* Scryer Prolog 0.9.1 */
?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
% CPU time: 0.000s error(existence_error(procedure,'$destroy_findall2_bag'/0),'$destroy_findall2_bag'/0).
?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
% CPU time: 32.102s
true.
Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 10:46:02 UTC+1:
Interesting replacement of setup_call_cleanup/3:
open(Path, read, Input),
catch(read_term(Input, Term, Options), Error, (close(Input),throw(Error))),
close(Input) https://github.com/LogtalkDotOrg/logtalk3/blob/master/library/term_io/term_io.lgt
Can we use this for something?
Here is some testing, with dry implementation of the bag:
/* SWI-Prolog 9.1.4 */
/* N215 Solution */
?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
% 7,000,000 inferences, 0.875 CPU in 0.871 seconds (100% CPU, 8000000 Lips)
true.
/* Logtalk Idiom */
?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
% 6,000,000 inferences, 0.500 CPU in 0.497 seconds (101% CPU, 12000000 Lips)
true.
Here is a proposal how to extend the Logtalk idiom by atomicity:
shield(
open(Path, read, Input),
catch(unshield(read_term(Input, Term, Options)), Error, (close(Input),throw(Error))),
close(Input)).
shield/1 is a new meta predicate inspired by Python:
awaitable asyncio.shield(aw )
Protect an awaitable object from being cancelled. https://docs.python.org/3/library/asyncio-task.html#shielding-from-cancellation
I guess it corresponds to sig_atomic/1 in SWI-Prolog and sys_atomic/1
in formerly Jekejeke Prolog. unshield/1 reverts shield/1, I didn’t find it yet
in some existing Prolog system. Disclaimer: The above idea of a
shielded Logtalk idiom is not yet practically tested.
Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 10:49:01 UTC+1:
Scryer Prolog isn't that lucky. Their setup_call_cleanup/3
has some meta predicate issue. And their catch/3 is utterly slow.
/* Scryer Prolog 0.9.1 */
?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
% CPU time: 0.000s error(existence_error(procedure,'$destroy_findall2_bag'/0),'$destroy_findall2_bag'/0).
?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
% CPU time: 32.102s
true.
Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 10:46:02 UTC+1:
Interesting replacement of setup_call_cleanup/3:
open(Path, read, Input),
catch(read_term(Input, Term, Options), Error, (close(Input),throw(Error))),
close(Input) https://github.com/LogtalkDotOrg/logtalk3/blob/master/library/term_io/term_io.lgt
Can we use this for something?
Here is some testing, with dry implementation of the bag:
/* SWI-Prolog 9.1.4 */
/* N215 Solution */
?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
% 7,000,000 inferences, 0.875 CPU in 0.871 seconds (100% CPU, 8000000 Lips)
true.
/* Logtalk Idiom */
?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
% 6,000,000 inferences, 0.500 CPU in 0.497 seconds (101% CPU, 12000000 Lips)
true.
Woa! My new setup_once_cleanup/3, which adopts the Logtalk idiom,
does something totally different, it overrides the primary exception.
This is incompatible with the usual setup_call_cleanup/3:
Logtalk idiom as is:
?- once_cleanup(true, throw(foo), throw(bar)).
Unknown exception: bar
?- catch(once_cleanup(true, throw(foo), throw(bar)), E, true).
E = bar.
Now compare with what some new Prolog systems do:
/* Trealla Prolog */
?- call_cleanup(throw(foo), throw(bar)).
throw(foo).
/* Scryer Prolog */
?- call_cleanup(throw(foo), throw(bar)).
throw(foo).
Now I found two more cases where I could
use the new setup_once_cleanup/3. These
correspond to the following in SWI-Prolog:
with_mutex/2:
The goal argument is onced. So an implementation
with setup_call_cleanup/3 is overkill, can be as well
implemented with setup_once_cleanup/3. I saw that
with_mutex/2 is implemented natively in SWI-Prolog
using callProlog, which I guess can be used to create
a setup_once_cleanup/3 behaviour.
Pitty the thingy isn’t named once_with_mutex/2. In
shared lazy tabling I have a strange case for a
setup_call_cleanup/3 based mutex handling. I guess I
will rename it to call_with_mutex/2, and also introduce a
once_with_mutex/2, and see to it that shared eager
tabling uses the new setup_once_cleanup/3. This is
a low priority long term change.
call_with_time_limit/2:
The goal argument here is onced as well. Pitty the
thingy isn’t name once_with_time_limit/2. I have a meta
predicate time_out/2 based on setup_call_cleanup/3 which
I can now migrate to setup_once_cleanup/3. But maybe I
will also rename it to once_with_time_limit/2. Oh the horror!
This is a high priority short term change.
Is Canada also France? Seems I am not the only one who got
into struggle with Logtalk sooner or later. LoL
How its started:
Ticket raised by me Aug 9, 2021 (when I was "ghost")
Feature request flag dialect, maybe version and version_data https://github.com/mthom/scryer-prolog/issues/1017
How its going:
Commit by pmoura last week
Delete Scryer Prolog support due to this system refusal to
support the de facto standard `version_data` flag https://github.com/LogtalkDotOrg/logtalk3/commit/d93883c5a8b014af09bd0e11439eaff30e1c1a5c
What happened?
LoL
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 490 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 62:19:12 |
| Calls: | 9,676 |
| Files: | 13,719 |
| Messages: | 6,171,618 |