Frédéric Blanqui
Frédéric Blanqui
I do not think that this a desirable feature. I would prefer to disallow it in LP. Any opinion?
Hi Jui-Hsuan. Thanks for your first PR! Note that this PR should modify the file sr.ml.
The set of equations is already computed by the type inference algorithm. You don't have to compute it again. The main problem is to turn this set of equations into...
Rodolphe, completion is very hard in general (harder than termination alone!). And, as we can already export rules to the TRS (for confluence) and XTC (for termination) formats, it should...
By the way, I see that the exports to TRS and XTC are not documented. @GuillaumeGen : could you please add a PR with at the beginning of termination.ml some...
@wujuihsuan2016 : there exist various completion tools. It would be good to try several.
Is there any restriction on identifiers in the XTC format? If not, as I suspect for XTC is an XML format, then there is no reason for changing names. This...
In the TRS format (see http://project-coco.uibk.ac.at/problems/trs.php), we have: >id is any nonempty sequence of characters not containing > whitespace > the characters ( ) " , | \ > the...
General remark: for computing critical pairs, do not use the unification algorithm implemented in unif.ml, but define your own syntactic first-order unification algorithm.
For the sake of simplicity and modularity, I propose to proceed in clearly distinct steps as follows: 1. Translate rule lhs's into terms by replacing pattern variables by fresh metavariables....