Deducteam
evaluation of lambda body
In the following example, the function (λ x, test x) is reduced to (λ x, C2), which seems strange as the parameter is unknown. I would expect the expression to be irreducible.
inductive #test: TYPE ≔
C1 : #test
| C2 : #test;
sequential symbol test: #test → #test;
rule test C1 ↪ C1
with test _ ↪ C2;
compute (λ x, test x);
Hi, for me, it has the correct behavior because you use an unnamed pattern variable test _, so it will unify with any term and use the modifier sequential.
But, because x is unknown, we cannot decide if x=C1 or not, so rule application should block.
Otherwise, reduction becomes non confluent: (λ x, test x) C1 --> C2 if body is reduced first and C1 if beta-reduction is applied first.
It's because you declared test as sequential. For sequential symbols, rules are tried in the order they are declared. In your example, x does not match C1 but it marches _. Using sequential symbols is not recommended: it may break some essential properties (the doc is explicit about this ;-)). Sequential symbols may be useful for some applications (e.g. reification) but their use must be restricted. You need to be very careful when using them.
Here I would say that we don't know if x matches C1 or not. We need sequential to write some meta level functions and we need default cases, those that are not covered by the abstract language. Don't know if it is possible to avoid its use...
Please provide more details and some example so that we can help you more if possible.
For example, looking for a given element in list of formulas (any lambdapi formula of a given type).
If I don't have equality on formulas: I would declare mem sequential and the rules:
rule mem $f ($f::_) --> true
with mem $f (_::$l) --> mem $f $l
with mem $f [] --> false
Right, you need mem to be sequential here. @NotBad4U and @melanie-taprogge do similar things to reify Lambdapi terms into some data types in the implementation of their reflexive tactics. I believe that it is fine as long as reification is used at the top level only. In the problem mentioned at the beginning, the sequential function is applied to a bound variable. Can you avoid this case?
My comment might be quite outdated (I was very aware of those kind of things 5 years ago, not anymore), but I still think that it might help understand the purpose of sequential.
There seems to be an ambiguity about the meaning of sequential. Its purpose is to give the users the possibility to add optimisations in the order rules are applied. It means "use the 3rd rule only if you are sure the 2nd one cannot be applied right now". But it does not mean "use the 3rd rule only if you are sure the 2nd one will never be applicable"
(Here "right now", means "after having normalized enough the arguments").
An example where it is useful is:
rule + 0 $y --> $y
with + $x 0 --> $x
with + (S $x) $y --> S (+ $x y)
Without the sequential keyword, the computation of + (fact 5) 0 would (probably) try to reduce the first argument to a weak head normal form, see that it is a successor and apply the 3rd rule, despite the second one being applicable.
If a rule is head applicable, then a rule will be head applied, no matter if you added sequential or not. The distinction is only which rule will be applied.
Especially it is not designed to make non-confluent rewrite systems confluent again.
What you seem to want is sequential to introduce what I called a "time-bomb", ie something which triggers later in the computation, when enough information have been computed to know in which branch we are.
The right solution to do so 5 years ago was to introduce such a symbol manually with the appropriate rewrite rules.
The "time-bomb" in your examples are quite simple, in the first one, it is just an explicit pattern:
symbol test: #test → #test;
rule test C1 ↪ C1
with test C2 ↪ C2;
or an equality decider:
rule mem $f ($g::$l) --> or (eq $f $g) (mem $f $l)
with mem $f [] --> false
where eq is a symbol which computes only if both arguments are "constructor headed values".
I have solved the issue by adding a tactic "#call f a" which allows delaying the evaluation of (f a) until the interpretation of #call:
In tactic.ml:
| T_call, [f;a] -> P_tac_eval (p_term pos idmap (mk_Appl (f,a)))