Deducteam
Conditional rewriting
I open this issue to discuss conditional rewriting as a possible feature request because I just heard of the following benchmark that might be of interest to compare the efficiency of Dedukti with programming languages: http://rec.gforge.inria.fr/.
- Is conditional rewriting desirable in Dedukti?
Apart from the mentioned benchmark, here are a few motivations for adding conditional rewriting.
- Encoding syntactic side-conditions
In the following example, we translate recursive ML programs using a fixpoint combinator. In order to preserve termination, we need to reduce the fixpoint only when it is applied to a value.
type : Type.
term : type -> Type.
Bool : type.
def bool := term Bool.
true : bool.
def and : bool -> bool -> bool.
[] and true true --> true.
Nat : type.
def nat := term Nat.
0 : nat.
S : nat -> nat.
Tree : Type.
def tree := term Tree.
leaf : nat -> tree.
node : tree -> tree -> tree.
def is_val : A : type -> term A -> bool.
[] is_val Nat 0 --> true
[n] is_val Nat (S n) --> is_val Nat n
[n] is_val Tree (leaf n) --> is_val Nat n
[l,r] is_val Tree (node l r) --> and (is_val Tree l) (is_val Tree r).
def fix : A : Type -> B : Type ->
((term A -> term B) -> term A -> term B) ->
term A -> term B.
[A, B, f, v] fix A B f v ? is_val A v == true --> f (fix A B f) v.
- Poor-man's modulo AC
Thanks to conditional rewriting, we can implement sorted lists:
bool : Type.
true : bool.
nat : Type.
0 : nat.
S : nat -> nat.
def lt : nat -> nat -> bool.
[] lt 0 (S _) --> true
[m,n] lt (S m) (S n) --> lt m n.
slist : Type.
nil : slist.
def cons : nat -> slist -> slist.
[a,b,l] cons a (cons b l) ? lt b a == true --> cons b (cons a l).
#ASSERT (cons 0 (cons (S 0) nil)) == (cons (S 0) (cons 0 nil)).
Note that cons a (cons b l) and cons b (cons a l) are not
convertible in general but we can prove by induction the theorem a : nat -> b : nat -> l : slist -> eq list (cons a (cons b l)) (cons b (cons a l)).
- Is it easy to encode?
Usually, when I want to use a rule of the form
[y1, ..., ym] f p1 ... pn ? t == t' --> a
(yi are variables, f is a definable, pi are patterns, t, t', and are terms).
what I do instead is that I declare a new definable f' and write the
following rules (note that the second is not linear):
[y1,...,ym] f p1 ... pn --> f' p1 ... pn t t'
[y1,...,ym,x] f' p1 ... pn x x --> a
I do not know what the limits of this trick are.
- Is it already there?
It seems that Dedukti already uses conditional rewriting internally but simply does not yet offer syntax for accessing this feature. Would it be hard to add this feature?
- Meta-theory with conditional higher-order rewriting?
Does conditional rewriting make harder proving good properties of the rewrite system? Harder than non-linearity alone?
On the technical side, I think adding conditional rewriting is not hard to implement in Dedukti. Moreover, I had the impression that it might be useful to express more theories (such as CTT for example).
Le 17/04/2018 à 08:34, Raphaël Cauderlier a écrit :
I open this issue to discuss conditional rewriting as a possible feature request because I just heard of the following benchmark that might be of interest to compare the efficiency of Dedukti with programming languages: http://rec.gforge.inria.fr/.
- Is conditional rewriting desirable in Dedukti?
Apart from the mentioned benchmark, here are a few motivations for adding conditional rewriting.
- Encoding syntactic side-conditions
In the following example, we translate recursive ML programs using a fixpoint combinator. In order to preserve termination, we need to reduce the fixpoint only when it is applied to a value.
It seems to be more than this: by doing so, you enforce some specific reduction strategy. As for termination alone, isn't there another solution? Isn't it enough to go through at least one match? Because checking that an argument is a value at each reduction step is VERY inefficient...
|type : Type. term : type -> Type. Bool : type. def bool := term Bool. true : bool. def and : bool -> bool -> bool. [] and true true --> true. Nat : type. def nat := term Nat. 0 : nat. S : nat -> nat. Tree : Type. def tree := term Tree. leaf : nat -> tree. node : tree -> tree -> tree. def is_val : A : type -> term A -> bool. [] is_val Nat 0 --> true [n] is_val Nat (S n) --> is_val Nat n [n] is_val Tree (leaf n) --> is_val Nat n [l,r] is_val Tree (node l r) --> and (is_val Tree l) (is_val Tree r). def fix : A : Type -> B : Type -> ((term A -> term B) -> term A -> term B) -> term A -> term B. [A, B, f, v] fix A B f v ? is_val A v == true --> f (fix A B f) v. |
- Poor-man's modulo AC
Thanks to conditional rewriting, we can implement sorted lists:
|bool : Type. true : bool. nat : Type. 0 : nat. S : nat -> nat. def lt : nat -> nat -> bool. [] lt 0 (S _) --> true [m,n] lt (S m) (S n) --> lt m n. slist : Type. nil : slist. def cons : nat -> slist -> slist. [a,b,l] cons a (cons b l) ? lt b a == true --> cons b (cons a l). #ASSERT (cons 0 (cons (S 0) nil)) == (cons (S 0) (cons 0 nil)). |
Note that |cons a (cons b l)| and |cons b (cons a l)| are not convertible in general but we can prove by induction the theorem |a : nat -> b : nat -> l : slist -> eq list (cons a (cons b l)) (cons b (cons a l))|.
- Is it easy to encode?
Usually, when I want to use a rule of the form
|[y1, ..., ym] f p1 ... pn ? t == t' --> a |
(yi are variables, f is a definable, pi are patterns, t, t', and are terms).
what I do instead is that I declare a new definable |f'| and write the following rules (note that the second is not linear):
|[y1,...,ym] f p1 ... pn --> f' p1 ... pn t t' [y1,...,ym,x] f' p1 ... pn x x --> a |
I do not know what the limits of this trick are.
You should have a look at the literature on conditional rewriting and their encodings into unconditional rewriting. See for instance https://doi.org/10.1007/978-3-540-31959-7_13 or more recent works perhaps.
- Is it already there?
It seems that Dedukti already uses conditional rewriting internally but simply does not yet offer syntax for accessing this feature. Would it be hard to add this feature?
I explained Dedukti's operational semantics in http://rewriting.gforge.inria.fr/divers/dedukti-op-sem.pdf. But it has perhaps been fixed since then because it was creating problems wrt confluence.
- Meta-theory with conditional higher-order rewriting?
Does conditional rewriting make harder proving good properties of the rewrite system?
Yes! For confluence, see http://dx.doi.org/10.1016/j.tcs.2009.07.058 . For termination, see http://dx.doi.org/10.1007/11916277_8 .
Harder than non-linearity alone?
It depends. Non-linearity is not a problem for termination. It is for confluence though. Conditional rewriting is a problem for both.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/Deducteam/Dedukti/issues/73, or mute the thread https://github.com/notifications/unsubscribe-auth/AKWYmRbY7ImkE8v_1nBYjLWXSIoGxCpGks5tpYzqgaJpZM4TXtgG.
I had the impression that it might be useful to express more theories (such as CTT for example).
In the case of CTT, I think it would help a bit but not much. To encode CTT easily we would need constraints of the form "type foo is inhabited" which is obviously not decidable in general.
Isn't it enough to go through at least one match?
I am not sure what you mean by this so let's take a concrete example: computing the list of all natural numbers between x (included) and y (excluded). The way I would write this function in ML is as follows:
let rec interval x y = if x >= y then [] else Cons(x, interval (S x) y)
It terminates and it makes sense so we do not want to reject this recursive definition. What should a translator for ML language to Dedukti (such as Focalide) do on this program?
-
simulate call-by-value as I proposed.
-
require a proof of termination. Let's say that the user (or an automated tool) provides the measure
(fun x y -> y - x), we can translate theintervalfunction as
def interval : nat -> nat -> list nat.
[x,y] interval x y ? (- y x) == 0 -->
(; the measure is 0 so the recursive branch is dead code,
we replace the recursive call by Nil ;)
if (geq x y) (Nil nat) (Cons nat x (Nil nat)).
[x,y] interval x y ? is_positive (- y x) == true --> if (geq x y) (Nil nat) (Cons nat x (interval (S x) y)).
If the function provided by the user is indeed a measure, the Dedukti rewrite system terminates but now we are computing the measure at each step which does not seem more efficient than checking that the arguments are values (it might be slower if the measure is not linear or quicker if it can return an S without fully evaluating its arguments).
- translate it by a non-terminating rewrite system. This is what Focalide actually does: simply check that they start with a constructor which corresponds to defining
is_vallike this:
def is_val : A : type -> term A -> bool.
[] is_val Nat 0 --> true
[] is_val Nat (S _) --> true
[] is_val (list _) (Nil _) --> true
[] is_val (list _) (Cons _ _ _) --> true.
[] is_val Tree (leaf _) --> true
[] is_val Tree (node _ _) --> true.
You should have a look at the literature on conditional rewriting and their encodings into unconditional rewriting
Thank you for the pointer.
Hello Raphaël.
Why not encoding your interval function as follows?
interval x y --> nil if x >= y -->* true
interval x y --> cons x (interval (s x) y) if x >= y -->* false
assuming for instance that >= is defined for instance as follows
x >= 0 --> true
s x >= s y --> x >= y
0 >= s y --> false
Frédéric.
Le 06/05/2018 à 15:22, Raphaël Cauderlier a écrit :
I had the impression that it might be useful to express more theories (such as CTT for example).In the case of CTT, I think it would help a bit but not much. To encode CTT easily we would need constraints of the form "type foo is inhabited" which is obviously not decidable in general.
Isn't it enough to go through at least one match?I am not sure what you mean by this so let's take a concrete example: computing the list of all natural numbers between |x| (included) and |y| (excluded). The way I would write this function in ML is as follows:
|let rec interval x y = if x >= y then [] else Cons(x, interval (S x) y)|
It terminates and it makes sense so we do not want to reject this recursive definition. What should a translator for ML language to Dedukti (such as Focalide) do on this program?
simulate call-by-value as I proposed.
require a proof of termination. Let's say that the user (or an automated tool) provides the measure |(fun x y -> y - x)|, we can translate the |interval| function as|def interval : nat -> nat -> list nat. [x,y] interval x y ? (- y x) == 0 --> (; the measure is 0 so the recursive branch is dead code, we replace the recursive call by Nil ;) if (geq x y) (Nil nat) (Cons nat x (Nil nat)). [x,y] interval x y ? is_positive (- y x) == true --> if (geq x y) (Nil nat) (Cons nat x (interval (S x) y)). |
If the function provided by the user is indeed a measure, the Dedukti rewrite system terminates but now we are computing the measure at each step which does not seem more efficient than checking that the arguments are values (it might be slower if the measure is not linear or quicker if it can return an S without fully evaluating its arguments).
- translate it by a non-terminating rewrite system. This is what Focalide actually does: simply check that they start with a constructor which corresponds to defining |is_val| like this:
|def is_val : A : type -> term A -> bool. [] is_val Nat 0 --> true [] is_val Nat (S _) --> true [] is_val (list _) (Nil _) --> true [] is_val (list _) (Cons _ _ _) --> true. [] is_val Tree (leaf _) --> true [] is_val Tree (node _ _) --> true. |
You should have a look at the literature on conditional rewriting and their encodings into unconditional rewritingThank you for the pointer.
— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/Deducteam/Dedukti/issues/73#issuecomment-386879102, or mute the thread https://github.com/notifications/unsubscribe-auth/AKWYmb8N4ANna3679yGIL-v96gNsAzRaks5tvvkjgaJpZM4TXtgG.
Here are a few reasons:
The main problem is that if-then-else is a local constructs wheras conditional rewriting is a toplevel construct so to translate the former to the latter, we would need to lift all the if-then-elses of the function and remember for each recursive call the conditions appearing on the path. Nothing dramatically hard here but it does not look very funny to implement.
Moreover, the translation that you propose is not linear: the condition x >= y is duplicated in the produced code. For this simple example it is not an issue because this term is very small and I would bet that in practice each if-then-else condition is small but if conditions are chained, this duplication can become problematic. Consider for example Euclidean algorithm:
let rec gcd a b =
let c = a - b in
if c < 0 then gcd b a else
if c = 0 then a else gcd c b
I guess that the translation scheme that you propose would give
def gcd : int -> int -> int.
[a,b] gcd a b ? (c => < c 0) (- a b) == true --> gcd b a
[a,b] gcd a b ? (c => and (not (< c 0)) (= c 0)) (- a b) == true --> a
[a,b] gcd a b ? (c => and (not (< c 0)) (not (= c 0))) (- a b) == true --> (c => gcd c b) (- a b).
In which the term < c 0 is copied 3 times and the term - a b is copied 4 times.
Last but not least, I do not see how to generalize this idea to pattern-matching.
@barras , are you planing to investigate more the embedding of CTT into Dedukti 2.x? Do you only use Dedukti 3 (aka lambdapi) now?