Encode simplify rule with a term rewriting systems

[NotBad4U]

The crate term-rewriting-rs could be use to defined some rewriting rules specified in Alethe. This lib is a Rust implementation of first-order term rewriting systems (TRS).

Here is an example of utilisation from the documentation on doc.rs:

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let term = parse_term(&mut sig, "J(F(C) K(C A))").expect("parse of J(F(C) K(C A))");

let rewritten_terms = &t.rewrite(&term, Strategy::Normal).unwrap();
assert_eq!(rewritten_terms.len(), 1);
assert_eq!(rewritten_terms[0].display(), "J(G K(C A))");

It could be a good alternative to writing all the simplification by hand in simplification.rs and having an algorithm that tries to compose them.

[HanielB]

Thanks for the suggestion, @NotBad4U! I agree that having something more general than what is currently at simplification.rs is a better path.

That said, I'm reticent of relying on an external library, specially one that does not seem to be actively maintained (last update was 4y ago). I prefer for Carcara to have its own term rewriting engine, which can be freely customizable by rules/strategies (note that in simplification.rs not only the rules but also the strategy is hard-corded, following the Alethe spec).

Another benefit of Carcara having its own rewriting engine is that it could be leverage for proof elaboration, not only for proof checking. So if one is interested in following a proof reconstruction approach for term rewriting, like the one described in this paper, Carcara could do it.

[NotBad4U]

Another benefit of Carcara having its own rewriting engine is that it could be leverage for proof elaboration, not only for proof checking. So if one is interested in following a proof reconstruction approach for term rewriting, like the one described in this paper, Carcara could do it.

The library term-rewriting-rs provides a trace of all the rewrites. it might be possible to do the reconstruction of simple things from this. I agree that this solution might only be able to cover simple simplification.

How is difficult to implement the algorithm described in this paper ? Is there already an implementation that maybe we can call by FFI?

[HanielB]

The library term-rewriting-rs provides a trace of all the rewrites. it might be possible to do the reconstruction of simple things from this. I agree that this solution might only be able to cover simple simplification.

Does it only give the rules that were used in the trace? One can get pretty far with this already, but depending on the rewriting strategy being applied we'd need more information. In cvc5 we actually covered things like this also in this other paper, section 4. The use case there was a bit different, as it also involved substitution and strategies.

How is difficult to implement the algorithm described in this paper ?

It should not be too difficult in principle. The implementation in cvc5 of the algorithm is about 1k loc in C++ and could serve as a reference.

Is there already an implementation that maybe we can call by FFI?

The implementation in cvc5 of the reconstruction for the Rare rules (the DSL in the above paper) is not exposed to the user, nor would it be too easy to do so atm. One of the difficulties is that cvc5 relies on having been compiled with the set of rewrite rules that are going to be used for the reconstruction. So I think that for Carcara it'd be best to have its ows implementation.

[hansjoergschurr]

Could the Carcara implementation use the same Rare rule database as cvc5? In cvc5 there afaik there is a Python script that generates the C++ code, maybe this can be hacked to generate Rust code for Carcara? Carcara would still need a rewrite engine, but that might simplify updates.
A downnside is that this results in some shared code between cvc5 and Carcare which is reduces the trustworthiness.

[bpandreotti]

I'm not sure how complex this Python script is, but it might be possible to instead write a Rust procedural macro to do this code generation

[HanielB]

Could the Carcara implementation use the same Rare rule database as cvc5?

I think this is a good starting point for this direction we are discussing. As for the code generation, I think this would better be done in a second phase.

I think the path forward for this is, at least initially, as @NotBad4U suggested, having a general term rewriting engine that is parameterized by rewrite rules. I just think that we should implement that in Carcara itself. So it's like building an interpreter for Rare rather than a compiler.

[NotBad4U]

@HanielB , where could I find the list of rules of the RARE database?
I just read the paper you mentioned, and I would like to make a POC.

[HanielB]

@HanielB , where could I find the list of rules of the RARE database? I just read the paper you mentioned, and I would like to make a POC.

I'm glad to hear you'd like to try that! The current RARE database of cvc5 can be found in the links below. That is including only the cvc5 theories that are supported in Alethe currently (so no strings or bit-vectors, for example).

• https://github.com/cvc5/cvc5/blob/proof-new/src/theory/builtin/rewrites
• https://github.com/cvc5/cvc5/blob/proof-new/src/theory/booleans/rewrites
• https://github.com/cvc5/cvc5/blob/proof-new/src/theory/uf/rewrites
• https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites

So that I understand better, what is it exactly that you are thinking of building a POC for? The checking of a given rewrite in an Alethe proof with a general term rewriting algorithm in Carcara that is parameterized by a set of read RARE rewrites?

[NotBad4U]

@HanielB could you point me to the Gradual type implementation?
Moreover, did you have to add a type inference mechanism? Because, if you take this rule

(define-rule* bool-and-true ((xs Bool :list) (ys Bool :list)) (and xs true ys) (and xs ys))

this rule expects two Bool :list but in Carcara we have only Term without an associated type, so we will need to infer the type of a term. Are you in the same case for CVC5?

[HanielB]

You mean to how the rule itself would be represented internally? Or for instances of the rule? Instances of the rule will not have lists "explicitly", i.e., it would be something like

(step t8 (cl (= (and p1 true true) (and p1 true))) :rule simplify :args (bool-and-true (p1) (true)))
(step t9 (cl (= (and p1 true) p1)) :rule simplify :args (bool-and-true (p1) ()))

Lists can be represented easily enough with Term with some builtin operator.

[NotBad4U]

Sorry if you misunderstand my question. My question was related to the typing system of RARE+CVC5. For example if you have the clause: and p1 p2 p3......, do you have some inference typing rules in RARE (or in CVC5) to infer that this term has the type Bool :list?

[HanielB]

It's more ad-hoc than that. In cvc5's type system the and operator is "n-ary", so the type of any (and t1 ... tn) term will vary depending on how many arguments are there (i.e. Bool -> ... -> Bool -> Bool). As for the RARE rules, when they are incorporated into cvc5 (this is done statically, with cvc5 being compiled together with a set of RARE rules), they are represented in a dedicated data structure to be used during the matching algorithm. So there is not really a question of how to type them.

The code in cvc5 for representing the RARE rules in in here:

https://github.com/cvc5/cvc5/blob/proof-new/src/rewriter/rewrite_db.h