Email Gateway (Aug 22 2022 at 15:39): Email Gateway (Aug 22 2022 at 15:39):From: Simon Wimmer <wimmersimon@gmail.com>
Dear list,
a student of mine is trying to build a little utility to automatically
provide memoized versions of a class of recursively defined functions (e.g.
for dynamic programming).
We are experimenting with a monadification style, which tries to lift a
function of type
('a => 'b) => 'c => 'd
to a function of type
(('a => 'b m) => ('c => 'd m) m) m.
This works quite nicely up to the point where we need to fundef_cong rules
for termination proofs.
Consider the following example:
fun f :: "nat ⇒ int" where
"f 0 = 0"
| "f (Suc i) = undefined (map f [0..<Suc i])"
If we use a lifted version of map of type
('a => 'b m) => 'a list => 'b list m,
then we can obtain a lifted version of f
fun f' :: "nat ⇒ int m" where
"f' 0 = return 0"
| "f' (Suc i) = undefined (map' f' [0..<Suc i])"
by using the following fundef_cong rule:
assumes "⋀x. x ∈ set xs ⟹ f x = g x" "xs = ys"
shows "map' f xs = map' g ys"
.
However, what we would really want is to use the combinator map'' of type
(('a => 'b m) => ('a list => 'b list m) m) m
like this
function f'' :: "nat ⇒ int m" where
"f'' 0 = return 0"
| "f'' (Suc i) = undefined (map'' . (return f'') . (return ([0..<Suc i])))"
(. is lifted application)
We tried to lift the fundef_cong rule to this setting by starting like this
assumes
"⋀x xs'. xs' ∈ set_state xs ⟹ x ∈ set xs' ⟹ f . (return x) = g . (return
x)" "xs = ys"
shows "map'' . f . xs = map'' . g . ys"
If we leave out the assumption, then the function package seems to be able
to apply the rule and presents us a trivial goal for termination.
However, we do not know how to phrase a correct rule that would be helpful
for the function package.
Does anyone have an idea on how this could be done?
Cheers,
Simon
DP_Lifting.thy
Monad.thy
Test_Map.thy
Email Gateway (Aug 22 2022 at 15:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Simon,
Here's a quick guess: In the conclusion of the premises of the fundef_cong rule, the
higher-order recursion variable still occurs as an argument to a function. In your
theories, I haven't seen any fundef_cong rule for the operator (.). So the function
package will use the congruence rule "cong" for dealing with (.), which loses the
connection between f and x. Have you tried adding a fundef congruence rule for (.), too?
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 15:39):From: Simon Wimmer <wimmersimon@gmail.com>
Thank you Andreas, your suggestion at least solved part of the problem.
I can use a rule like this to get through the termination proof:
assumes
"⋀x xs'. xs' ∈ set_state xs ⟹ x ∈ set xs' ⟹ f x = g x" "xs = ys"
shows "map⇩T . (return f) . xs = map⇩T . (return g) . ys"
However, I was not able to define a fundef congruence rule for (.).
Trying something like this (not sure if this is correct), gives me an error
for COMP in the function command:
assumes
"⋀ f' g' x' y'. f' ∈ set_state f ⟹ g' ∈ set_state g ⟹ x' ∈ set_state x
⟹ y' ∈ set_state y
⟹ f' x' = g' y'"
shows "f . x = g . y"
Cheers,
Simon
Email Gateway (Aug 22 2022 at 15:39):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Simon,
Your congruence rule for (.) has the problem that the variables in the conclusion of the
congruence rule do not show up in the conclusion of the premise. The function package uses
these rules to infer the context in which a function all occurs. When it applies your new
rule to a schematic goal like
(map_T . (return f)) . xs = ?rhs
then the next subgoal will look like
!!f' g' x' y'. [| ... |] ==> f' x' = g' y'
where there are no more recursive calls in the conclusion. Thus, it thinks that it has now
found all of them, which obviously is not true and later leads to the error, because the
recursive call has moved to the assumptions of the goal state.
Best,
Andreas
Last updated: May 06 2024 at 16:21 UTC