lambdapi
lambdapi copied to clipboard
Deducteam
Wrong encoding in TRS or bug in CSI^ho
The following LambdaPi code
symbol cmd : TYPE; symbol value : TYPE;
symbol union : cmd → cmd → cmd ; symbol bind : cmd → (value → cmd) → cmd;
rule bind $c (λ x, union $F1.[x] $F2.[x]) ↪ union (bind $c (λ x, $F1.[x])) (bind $c (λ x, $F2.[x])) ;
get translated with --confluence to a .trs file that is reported by CSI^ho to be non-confluent. However, that's only because something wrong happens. I.e. the TRS rule expects (the encoding of) $F1 to be applied via "app" to x, and the critical pair found by CSI^ho comes from a (\lambda z. y z) x that may be reduced to just y x, where the latter is not syntactically of the form (app ? x).
How should I interpret it? Is it a bug/limitation in the way the .trs file is obtained? Is it a bug/limitation of CSI^/ho? Am I doing something wrong or am I missing something in my code?
Cheers, C.S.C.
The current code for exporting HRS is buggy. Please use https://github.com/Deducteam/lambdapi/pull/871 instead. It should be merged into master very soon. By the way, did you succeed in compiling CSI^ho or do you use the web interface? If you succeeded in compiling it, could you please tell which version of ocaml did you use?
Well, README says to use OCaml 3.12 (very old!). But I get the following error:
In file included from gpw/glueminisat/core/Solver.h:28,
from gpw/Solver.h:25,
from gpw/PbSolver.h:24,
from gpw/PbParser.h:23,
from gpw/PbParser.C:20:
gpw/glueminisat/core/SolverTypes.h:50:16: error: friend declaration of ‘GlueMiniSat::Lit mkLit(GlueMiniSat::Var, bool)’ specifies default arguments and isn’t a definition [-fpermissive]
50 | friend Lit mkLit(Var var, bool sign = false);
| ^~~~~
gpw/glueminisat/core/SolverTypes.h:58:14: error: friend declaration of ‘GlueMiniSat::Lit GlueMiniSat::mkLit(GlueMiniSat::Var, bool)’ specifies default arguments and isn’t the only declaration [-fpermissive]
58 | inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
| ^~~~~
gpw/glueminisat/core/SolverTypes.h:50:16: note: previous declaration of ‘GlueMiniSat::Lit GlueMiniSat::mkLit(GlueMiniSat::Var, bool)’
50 | friend Lit mkLit(Var var, bool sign = false);
| ^~~~~
Do you have any idea on how to solve this? Not sure it is possible if it relies on very old libraries...
The output is now:
(FUN
A : t -> t -> t
L : t -> (t -> t) -> t
P : t -> (t -> t) -> t
B : t -> t -> (t -> t) -> t
tests_OK_883_bind : t
tests_OK_883_union : t
tests_OK_883_value : t
)
(VAR
$x : t
$y : t -> t
$z : t
$1_3 : t -> t
$1_0 : t
$1_2 : t -> t
$1_0 : t
$1_3 : t -> t
$1_2 : t -> t
$1_1 : t
$1_0 : t
47 : t
48 : t
49 : t
)
(RULES
A(L($x,$y),$z) -> $y($z),
B($x,$z,$y) -> $y($z),
A(A(tests_OK_883_bind,$1_0),L($1_1,\47.A(A(tests_OK_883_union,$1_2(47)),$1_3(47)
))) -> A(A(tests_OK_883_union,A(A(tests_OK_883_bind,$1_0),L(tests_OK_883_value,\
48.$1_2(48)))),A(A(tests_OK_883_bind,$1_0),L(tests_OK_883_value,\49.$1_3(49))))
)
The web interface of CSI^ho (http://colo6-c703.uibk.ac.at/csi/index.php) returns:
YES
Problem:
A (L $x $y) $z -> $y $z
B $x $z $y -> $y $z
A (A tests_OK_883_bind $1_0) (L $1_1 (\47. A (A tests_OK_883_union ($1_2 47)) ($1_3 47))) ->
A (A tests_OK_883_union (A (A tests_OK_883_bind $1_0) (L tests_OK_883_value (\48. $1_2 48))))
(A (A tests_OK_883_bind $1_0) (L tests_OK_883_value (\49. $1_3 49)))
Proof:
Modularity Decomposition:
0:B $x $z $y -> $y $z
1:A (L $x $y) $z -> $y $z
A (A tests_OK_883_bind $1_0) (L $1_1 (\47. A (A tests_OK_883_union ($1_2 47)) ($1_3 47))) ->
A (A tests_OK_883_union (A (A tests_OK_883_bind $1_0) (L tests_OK_883_value (\48. $1_2 48))))
(A (A tests_OK_883_bind $1_0) (L tests_OK_883_value (\49. $1_3 49)))
-----
0:B $x $z $y -> $y $z
Higher-Order Church Rosser Processor:
B $x $z $y -> $y $z
critical peaks: 0
Higher-Order Closedness Processor:
all critical pairs are trivial
Qed
1:A (L $x $y) $z -> $y $z
A (A tests_OK_883_bind $1_0) (L $1_1 (\47. A (A tests_OK_883_union ($1_2 47)) ($1_3 47))) ->
A
(A tests_OK_883_union (A (A tests_OK_883_bind $1_0) (L tests_OK_883_value (\48. $1_2 48))))
(A (A tests_OK_883_bind $1_0) (L tests_OK_883_value (\49. $1_3 49)))
Higher-Order Church Rosser Processor:
A (L $x $y) $z -> $y $z
A (A tests_OK_883_bind $1_0) (L $1_1 (\47. A (A tests_OK_883_union ($1_2 47)) ($1_3 47))) ->
A
(A tests_OK_883_union (A (A tests_OK_883_bind $1_0) (L tests_OK_883_value (\48. $1_2 48))))
(A (A tests_OK_883_bind $1_0) (L tests_OK_883_value (\49. $1_3 49)))
critical peaks: 0
Higher-Order Closedness Processor:
all critical pairs are trivial
Qed
I continue with this bug, even if I am now using #871. I attach the code for the lambdapi project.
CSI^ho gives me the following critical pair proof. The pair is supposed to be joinable in lambdapi. There is an issue with the encoding at work. In particular the issue is the following rule:
bind $c (λ x, union $F1.[x] $F2.[x]) ↪ union (bind $c (λ x, $F1.[x])) (bind $c (λ x, $F2.[x]))
that becomes
(RULES app(app(c_ricciotti_riccio_bind,$0),lam(m_typ,\x.app(app(c_ricciotti_riccio_union,app($2,x)),app($3,x)))) -> app(app(c_ricciotti_riccio_union,app(app(c_ricciotti_riccio_bind,$0),lam(c_ricciotti_riccio_value,\x.app($2,x)))),app(app(c_ricciotti_riccio_bind,$0),lam(c_ricciotti_riccio_value,\x.app($3,x)))))
I.e. "$F1.[x]" becomes "app($2,x)".
However, this is NOT the right encoding when $2 is a generic term (e.g. a lambda-abstraction), like the non-joinable conversion below shows. In particular, the term in the first line SHOULD be rewritten, but it cannot because (66 70) is in place of the "expected" (app 66 70).
Higher-Order Nonconfluence Processor: non-joinable conversion: app (app c_ricciotti_riccio_bind $0) (lam m_typ (\70. app (app c_ricciotti_riccio_union (66 70)) (app $3 70))) <- app (app c_ricciotti_riccio_bind $0) (lam m_typ (\69. app (app c_ricciotti_riccio_union (app (lam 65 (\v_x. 66 v_x)) 69)) (app $3 69))) -> app (app c_ricciotti_riccio_union (app (app c_ricciotti_riccio_bind $0) (lam c_ricciotti_riccio_value (\67. app (lam 65 (\v_x. 66 v_x)) 67)))) (app (app c_ricciotti_riccio_bind $0) (lam c_ricciotti_riccio_value (\68. app $3 68))) ->* app (app c_ricciotti_riccio_union (app (app c_ricciotti_riccio_bind $0) (lam c_ricciotti_riccio_value (\67. 66 67)))) (app (app c_ricciotti_riccio_bind $0) (lam c_ricciotti_riccio_value (\68. app $3 68))) Qed
Quick observation: if I patch by hand the HRS file replacing in the rewriting rule "(app $2 x)" with "($22 x)" for "$22 : term -> term" and similarly for $33, then the critical pair disappears as expected. This is equivalent to encoding "$F.[x]" with "($F x)", i.e. at the meta-meta-level.
Note: the encoding ignores the associative and commutative attributes I have for "union" in the LP file. Probably it is CSI^ho that cannot handle AC, I suppose. If I add by hand commutativity in the HRS file CSI^ho resolves the critical pairs if I don't feed it all rules, or it timeouts with all rules. This is probably the gameover of my experiment, isn't it?
Side remarks:
Remark 1: the generated code in your last comments and targz file does not seem up to date (there should be no m_typ in the output). But this doesn't solve all the problems.
Remark 2: your system can be confluent modulo AC only. But LP critical pairs checking does not handle AC symbols currently, nor higher-order variables like F1 and F2. See https://lambdapi.readthedocs.io/en/latest/commands.html?highlight=critical%20pair#rule. So that's normal that LP doesn't complain.
Remark 3: concerning the confluence of this kind of systems, you may have a look at Hamana's work and tool SOL. See http://www.cs.gunma-u.ac.jp/~hamana/.
Remark 4: I don't know if CSI^ho can handle AC symbols.
On remark 1: I generated the file using the master branch of #871 I have just checked again and I am up-to-date. The SHA1 ID of the last commit is: 2933ac40c75a53b773b421a7069741c5aa07c0a8
On remark 2: I misunderstood the manual. From the manual it seems that the two limitations (AC and non-nullary pattern variables) are limitations of LambdaPi and not of the generated HRS files. Indeed the paragraph above that talks about --confluence does not mention the limitation and "lambdapi --confluence" does not print any warning. Maybe you should add warnings to --confluence and change the manual? (Unless you misunderstood that I was referring to CSI^ho only)
On remark 3: thanks, I will try!
Right, AC and non-nullary pattern variables are a current limitation of LP only.
The HRS export should be correct but AC is not part of the HRS format, is it? See http://project-coco.uibk.ac.at/problems/hrs.php.
The command to export to HRS should be: lambdapi export -o hrs file.lp > file.hrs.
Please, do not use --confluence. I am not sure it is working, and will probably be removed when #871 will be merged.
Using the export command, I get:
(FUN
A : t -> t -> t
L : t -> (t -> t) -> t
P : t -> (t -> t) -> t
B : t -> t -> (t -> t) -> t
ricciotti_riccio_bind : t
ricciotti_riccio_empty : t
ricciotti_riccio_singl : t
ricciotti_riccio_union : t
ricciotti_riccio_value : t
)
(VAR
$x : t
$y : t -> t
$z : t
$1_0 : t
$1_1 : t
$1_2 : t -> t
$1_3 : t -> t
$2_0 : t
$2_1 : t
$2_2 : t
$3_0 : t
$3_1 : t
$4_0 : t
$4_1 : t
$5_0 : t
77 : t
78 : t
79 : t
80 : t
)
(RULES
A(L($x,$y),$z) -> $y($z),
B($x,$z,$y) -> $y($z),
A(A(ricciotti_riccio_bind,$1_0),L($1_1,\77.A(A(ricciotti_riccio_union,$1_2(77)),$1_3(77)))) -> A(A(ricciotti_riccio_union,A(A(ricciotti_riccio_bind,$1_0),L(ricciotti_riccio_value,\78.$1_2(78)))),A(A(ricciotti_riccio_bind,$1_0),L(ricciotti_riccio_value,\79.$1_3(79)))),
A(A(ricciotti_riccio_bind,A(A(ricciotti_riccio_union,$2_0),$2_1)),$2_2) -> A(A(ricciotti_riccio_union,A(A(ricciotti_riccio_bind,$2_0),$2_2)),A(A(ricciotti_riccio_bind,$2_1),$2_2)),
A(A(ricciotti_riccio_bind,A(ricciotti_riccio_singl,$3_0)),$3_1) -> A($3_1,$3_0),
A(A(ricciotti_riccio_bind,$4_0),L($4_1,\80.ricciotti_riccio_empty)) -> ricciotti_riccio_empty,
A(A(ricciotti_riccio_bind,ricciotti_riccio_empty),$5_0) -> ricciotti_riccio_empty,
A(A(ricciotti_riccio_union,ricciotti_riccio_empty),ricciotti_riccio_empty) -> ricciotti_riccio_empty
)
As you can see, higher-order pattern variables are translated as you suggested. If you give this system (after some simple renamings) to the web interface of CSI^ho, you get:
NO
Problem:
A (L $x $y) $z -> $y $z
A (A bind $1_0) (L $1_1 (\77. A (A union ($1_2 77)) ($1_3 77))) ->
A (A union (A (A bind $1_0) (L value (\78. $1_2 78))))
(A (A bind $1_0) (L value (\79. $1_3 79)))
A (A bind (A (A union $2_0) $2_1)) $2_2 ->
A (A union (A (A bind $2_0) $2_2)) (A (A bind $2_1) $2_2)
A (A bind (A singl $3_0)) $3_1 -> A $3_1 $3_0
A (A bind $4_0) (L $4_1 (\80. empty)) -> empty
A (A bind empty) $5_0 -> empty
A (A union empty) empty -> empty
Proof:
Higher-Order Church Rosser Processor:
A (L $x $y) $z -> $y $z
A (A bind $1_0) (L $1_1 (\77. A (A union ($1_2 77)) ($1_3 77))) ->
A (A union (A (A bind $1_0) (L value (\78. $1_2 78))))
(A (A bind $1_0) (L value (\79. $1_3 79)))
A (A bind (A (A union $2_0) $2_1)) $2_2 ->
A (A union (A (A bind $2_0) $2_2)) (A (A bind $2_1) $2_2)
A (A bind (A singl $3_0)) $3_1 -> A $3_1 $3_0
A (A bind $4_0) (L $4_1 (\80. empty)) -> empty
A (A bind empty) $5_0 -> empty
A (A union empty) empty -> empty
critical peaks: 14
A (A union (A (A bind (A (A union 308) 309)) (L value (\78. 311 78))))
(A (A bind (A (A union 308) 309)) (L value (\79. 312 79))) <-[]->
A (A union (A (A bind 308) (L 310 (\77. A (A union (311 77)) (312 77)))))
(A (A bind 309) (L 310 (\77. A (A union (311 77)) (312 77))))
A (A union (A (A bind (A singl 369)) (L value (\78. 371 78))))
(A (A bind (A singl 369)) (L value (\79. 372 79))) <-[]->
A (L 370 (\77. A (A union (371 77)) (372 77))) 369
A (A union (A (A bind empty) (L value (\78. 445 78))))
(A (A bind empty) (L value (\79. 446 79))) <-[]-> empty
A (A union (A (A bind 514) (L 516 (\77. A (A union (517 77)) (518 77)))))
(A (A bind 515) (L 516 (\77. A (A union (517 77)) (518 77)))) <-[]->
A (A union (A (A bind (A (A union 514) 515)) (L value (\78. 517 78))))
(A (A bind (A (A union 514) 515)) (L value (\79. 518 79)))
A (A union (A (A bind 637) (L 639 (\80. empty)))) (A (A bind 638) (L 639 (\80. empty))) <-[
]-> empty
A (L 715 (\77. A (A union (716 77)) (717 77))) 714 <-[]->
A (A union (A (A bind (A singl 714)) (L value (\78. 716 78))))
(A (A bind (A singl 714)) (L value (\79. 717 79)))
A (L 805 (\80. empty)) 804 <-[]-> empty
empty <-[]->
A (A union (A (A bind 896) (L 898 (\80. empty)))) (A (A bind 897) (L 898 (\80. empty)))
empty <-[]-> A (L 932 (\80. empty)) 931
empty <-[]-> empty
empty <-[]->
A (A union (A (A bind empty) (L value (\78. 1010 78))))
(A (A bind empty) (L value (\79. 1011 79)))
empty <-[]-> empty
A (A bind $1_0) (L $1_1 (\77. empty)) <-[1,1,0]->
A (A union (A (A bind $1_0) (L value (\78. empty)))) (A (A bind $1_0) (L value (\79. empty)))
A (A bind empty) $2_2 <-[0,1,1]-> A (A union (A (A bind empty) $2_2)) (A (A bind empty) $2_2)
Higher-Order Nonconfluence Processor:
non-joinable conversion:
A
(A union
(A (A union (A (A bind 308) (L value (\78. 311 78)))) (A (A bind 309) (L value (\78. 311 78)))))
(A (A union (A (A bind 308) (L value (\79. 312 79)))) (A (A bind 309) (L value (\79. 312 79)))) *<-
A (A union (A (A bind (A (A union 308) 309)) (L value (\78. 311 78))))
(A (A bind (A (A union 308) 309)) (L value (\79. 312 79))) <- A (A bind (A (A union 308) 309))
(L 310
(\
77.
A (A union (311 77)) (312 77))) ->
A (A union (A (A bind 308) (L 310 (\77. A (A union (311 77)) (312 77)))))
(A (A bind 309) (L 310 (\77. A (A union (311 77)) (312 77)))) ->*
A
(A union
(A (A union (A (A bind 308) (L value (\78. 311 78)))) (A (A bind 308) (L value (\79. 312 79)))))
(A (A union (A (A bind 309) (L value (\78. 311 78)))) (A (A bind 309) (L value (\79. 312 79))))
Qed
After some renamings, the critical pair is:
A (A union
(A (A union
(A (A bind x) (L y)))
(A (A bind z) (L y))))
(A (A union
(A (A bind x) (L t)))
(A (A bind z) (L t)))
*<-
A (A union
(A (A bind (A (A union x) z)) (L y)))
(A (A bind (A (A union x) z)) (L t))
<-
A (A bind (A (A union x) z)) (L 310 (\u. A (A union (y u)) (t u)))
->
A (A union
(A (A bind x) (L 310 (\u. A (A union (y u)) (t u)))))
(A (A bind z) (L 310 (\u. A (A union (y u)) (t u))))
->*
A (A union
(A (A union
(A (A bind x) (L y)))
(A (A bind x) (L t))))
(A (A union
(A (A bind z) (L y)))
(A (A bind z) (L t)))
It is joinable modulo AC only.
I managed to obtain your output; adding by hand AC and dropping some rules CSI^ho manages. With all the rules it timeouts.
About recompilation: the errors you have can be bypassed adding "-fpermissive" to the CFLAGS in several Makefiles, e.g. CFLAGS = -Wall -ffloat-store -fpermissive in src/logic/src/gpw/Makefile
I managed to reach the final linking phase with issues with camlidl, but I get errors while linking at the very end. The errors are unrelated to -fpermissive. Let me know if you manage to recompile it because I would like to start it with a timeout much higher than 60s to see if it manages.
I got this message from Fabian Mitterwallner @fabeulous but didn't have the time to test it yet:
Dear Frédéric,
I believe CSI^ho is unfortunately no longer maintained. However, since the error you quote appears to be in a part of the source related to CSI/TTT2 I might be able to help.
I was able to compile CSI^ho from the source archive available on the website (http://cl-informatik.uibk.ac.at/software/csi/ho/) with the relatively recent OCaml version 4.13.1. Some small changes are required in the file 'src/util/src/listx.ml', which I have attached as a patch-file. You can apply it by running:
patch -p1 < path/to/csiho-ocaml-4.13.1.patch
in the freshly unpacked 'csiho' directory. Running
make dist-clean
followed by
DISABLE_Gpw=1 make
should successfully build CSI^ho. Setting 'DISABLE_Gpw=1' prevents the error you're seeing by simply not building the GPW solver. Fortunately it seems to be unused in CSI^ho, as far as I could tell.
I hope this helped?
Best,
Fabian