ceta(2) - selective context closure?
Dear all, can I express in CPF (for Ceta-2) that I want to apply "flat context closure" to a subset of rules only? specifically, I want this for rules with empty lhs or rhs, as it seems to increase the power of matrix interpretations. (as shown by Aprove in TC 23). I am looking at http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/8250228... but the example seems to close all rules. I guess I can indeed context-close all rules uniformly, and use the same interpretation, to remove the same rules. But perhaps I want other methods that refer to the original rules. Well it's a bit late anyway. - J.
Hi Johannes, I think you can do that: here is the IsaFoR/CeTA-code that checks correct application "check_rule_preserving fcs rs' rule ≡ ( check ((Bex (set rs') (instance_rule rule)) ∨ (∀C∈set fcs. Bex (set rs') (instance_rule (C⟨fst rule⟩, C⟨snd rule⟩)))) (showsl_lit (STR ''the rule '') ∘ showsl_rule rule ∘ showsl_lit (STR '' is neither contained in the resulting set of rules nor closed under all flat contexts⏎'')) so, for each “rule" in R, it is tested whether that rule is in R’, or the full context-closure of that rule is in R’ (modulo variable-renamings via “instance_rule”) Since I did not change the code of FCCs for CeTA 2.46 and CeTA 3.1, this should work, but please test beforehand. Best, René
Am 17.06.2024 um 14:42 schrieb Johannes Waldmann <johannes.waldmann@htwk-leipzig.de>:
Dear all,
can I express in CPF (for Ceta-2) that I want to apply "flat context closure" to a subset of rules only?
specifically, I want this for rules with empty lhs or rhs, as it seems to increase the power of matrix interpretations. (as shown by Aprove in TC 23).
I am looking at http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/8250228... but the example seems to close all rules.
I guess I can indeed context-close all rules uniformly, and use the same interpretation, to remove the same rules. But perhaps I want other methods that refer to the original rules.
Well it's a bit late anyway.
- J.
_______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
so, for each “rule" in R, it is tested whether that rule is in R’, or the full context-closure of that rule is in R’ (modulo variable-renamings via “instance_rule”)
Since I did not change the code of FCCs for CeTA 2.46 and CeTA 3.1, this should work, but please test beforehand.
yes, this seems to work. Thank you! - Johannes.
participants (2)
-
Johannes Waldmann -
Thiemann, René