Deducteam
Use the compute command to define a rule LHS ?
Currently, it is not possible to write rewrite rule such as:
[a] f (double 0) a --> a.
where double 0 reduces to S (S 0). Because this rule will never be matched. Instead, the user needs to write
[a] f (S (S 0)) a --> a.
This is not a real issue when the normal form is small. But it might be convenient to have a way to allow the first rewrite rule with the expected behavior. What I would propose, is to prefix arguments which should be normalized with a symbol such as > (assuming that this symbol is not allowed for identifiers). For example:
[a] f >(double 0) a --> a.
In that case, Dedukti should replace double 0 by its normal form before adding this rule to the signature.
We could also extend this feature with a warning when an argument of a rewrite rule is not in normal form. In that case, the rule will never be applied in this is probably not intended.
Hello François. Note that, if you add the rule with double, and double is defined, then you have a (local) confluence problem: for your system to be confluent, you should also have a rule f (s(s 0)) a --> a.
Hi all,
If I understood well, there would be no confluence problem with what @francoisthire is suggesting, as what he wants is just some syntactic sugar.
When a user adds the rule
[a] f >(double 0) a --> a.
it would in fact (only) add the following rule to the signature :
[a] f (S (S 0)) a --> a.
because the system knows from the > symbol that it has to normalize this argument before registering the rule.
Of course, if it would be more than this syntactic sugar (i.e. effectively registering a rule that contains a sub-term not in normal form like (double 0)), then we would have to also add all the rules that would correspond to the different evaluation strategies, but this is not what @francoisthire was suggesting I think.
PS : By the way, the name "double" in this example was a little bit weird, as it adds two instead of doubling its argument :)
Currently, the main issue I have is that there is no warning. It is convenient to have a warning by lambdapi when by typing, it knows that the LHS is not typable, hence it probably means that you've made a mistake.
Here the typing is correct but there is no way if double is defined that a term triggers this rule which is kind of strange the first time you encounter this behavior.
Currently, I manage to get around this issue, but it is a little bit annoying, I don't have "big" terms. Or "big" meaning annoying to write by hand.
However, while writing arithmetics proofs with rewrite rules as it was the plan a few months ago, I would not be surprised if that kind of issue comes out at some point.
Lambdapi emits a warning if it detects that the LHS cannot be typable. It cannot emit a warning each time it finds out that a LHS is typable only under some constraints as it happens often.
That the rule with double may not be applied is not related to typing but to the reduction strategy. As the reduction strategy should be complete (if the system is confluent), this should not be a problem.
Finally, concerning proofs, note that, in Lambdapi, proofs are built by using tactics. So, I don't see why the user would have to write rules with "big" non-normal subterms. No rule can be added in the environment when doing a proof.
That the rule with double may not be applied is not related to typing but to the reduction strategy. As the reduction strategy should be complete (if the system is confluent), this should not be a problem.
Well, the problem is to help the user to debug the Dedukti file he wrote. As I said, it is more or less only syntactic sugar so of course it is not needed and it probably never be, but it might be misleading for the user. I am just saying that, at least, warning the user if its rule cannot be applied might be helpful to debug a program.
Finally, concerning proofs, note that, in Lambdapi, proofs are built by using tactics. So, I don't see why the user would have to write rules with "big" non-normal subterms. No rule can be added in the environment when doing a proof.
Well, it depends what you want to add as rewrite rule for proving things. My point is that if for some reason, you want to add a rule where the LHS depends on the proof of some theorem... Well, you might encounter some difficulties to write it down. It might happen also that the left pattern of the rule needs to mention a defined symbol.
That last point is more about speculation. However, I am mostly saying that if such syntactic sugar is not wanted, having a warning from the system might be helpful and it is really easy to implement with a cheap cost. And if you judge that there should be no warning, IMHO, there should be at least a line or a paragraph we can refer to about that specific behavior.