Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Modular definition of type class constants for...

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Lars Hupel <hupel@in.tum.de>
Assume the following simple type class:

class foo =
fixes count :: "'a ⇒ nat"

Instantiations for simple recursive data types are trivial:

instantiation list :: (foo) foo
begin
fun count_list where
"count [] = 0" |
"count (x # xs) = count x + count xs"

instance ..
end

Now, consider a more elaborate data type:

datatype_new 'a rose = Fork 'a "'a rose list"

The naive attempt to instantiate "foo" for "rose" fails, as I expected:

instantiation rose :: (foo) foo
begin
fun count_rose where
"count (Fork a as) = count a + count as"

instance ..
end

My question is: How to define "count_rose" in such a way that I don't
have to repeat large parts of "count_list"?

The ultimate goal is to derive these instances automatically. I know
about the relevant AFP entry
(<http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml>),
but as far as I can see, it builds on the old datatype package, and I'd
rather like to have something for the new BNF package.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,

instantiation list :: (foo) foo
begin
fun count_list where
"count [] = 0" |
"count (x # xs) = count x + count xs"

instance ..
end

datatype_new 'a rose = Fork 'a "'a rose list"

The naive attempt to instantiate "foo" for "rose" fails, as I expected:

instantiation rose :: (foo) foo
begin
fun count_rose where
"count (Fork a as) = count a + count as"

instance ..
end

the best way to approach this is to replace count_rose mentally by a
syntactically different operation f and write down a specification for f
accordingly. This then should be transferable to an instantiation.

The ultimate goal is to derive these instances automatically. I know about the relevant AFP entry (<http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml>), but as far as I can see, it builds on the old datatype package, and I'd rather like to have something for the new BNF package.

Well, sounds there is some work to do there.

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Lars,

Am 10.06.2014 um 18:50 schrieb Lars Hupel <hupel@in.tum.de>:

Now, consider a more elaborate data type:

datatype_new 'a rose = Fork 'a "'a rose list"

The naive attempt to instantiate "foo" for "rose" fails, as I expected:

instantiation rose :: (foo) foo
begin
fun count_rose where
"count (Fork a as) = count a + count as"

instance ..
end

My question is: How to define "count_rose" in such a way that I don't have to repeat large parts of "count_list"?

Here's one way, perhaps:

class foo =
fixes count :: "'a => nat"

instantiation nat :: foo
begin
definition count_nat where "count n = n"

instance ..
end

instantiation list :: (foo) foo
begin
primrec count_list where
"count [] = 0" |
"count (x # xs) = count x + count xs"

instance ..
end

datatype_new 'a rose = Fork 'a "'a rose list"

instantiation rose :: (foo) foo
begin
primrec count_rose where
"count (Fork a as) = count a + count (map count as)"

instance ..
end

Notice that the above solution works with "primrec" -- no ad hoc termination arguments! But it does cheat a little bit in "count (map count as)", first counting the elements of the list, then counting the list of nats.

You might want to take a look at the BNF-based size extension. Try

thm list.size
thm rose.size

to see what it has to offer. I suspect that you could base "count" on "size_xxx" (e.g. "size_list"). If not, the idiom used to derive "size" systematically for all BNF-based datatypes might still serve as an inspiration.

Another possible source of inspiration is our sketch for a "countable" extension to BNF datatypes. I'm attaching the theory file. This development is somewhat simpler than the "size" extension, because it doesn't need to maintain two series of symbols in parallel (e.g. "size" instances vs. "size_xxx"). Hence, it appears to be a better model for what you want to do (assuming the "count (map count as)" cheat works for you).

The ultimate goal is to derive these instances automatically. I know about the relevant AFP entry (<http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml>), but as far as I can see, it builds on the old datatype package, and I'd rather like to have something for the new BNF package.

The author of this entry is all in favor of porting it to the new package, and it is, from what I understand, only a matter of time until he gets to it. ;)

Jasmin
BNF_LFP_Countable.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,

instantiation rose :: (foo) foo
begin
primrec count_rose where
"count (Fork a as) = count a + count (map count as)"

instance ..
end

thanks, but my real type class is a little bit more complicated. I
guess I should've posted the real thing from the beginning ;-)

class evaluate =
fixes eval :: "rule set ⇒ term ⇒ 'a ⇒ bool" ("_/ ⊢/ (_ ↓/ _)"
[50,0,50] 50)
assumes ...

Instantiations typically look like this:

instantiation list :: (evaluate) evaluate
begin
primrec eval_list where
"eval_list rs t [] ⟷ rs ⊢ t ⟶* Const ''List.list.Nil''" |
"eval_list rs t (x # xs) ⟷ (∃t⇩1 t⇩2. rs ⊢ t⇩1 ↓ x ∧ rs ⊢ t⇩2 ↓ xs ∧
rs ⊢ t ⟶* Const ''List.list.Cons'' $ t⇩1 $ t⇩2)"

...

end

Off the top of my head, I don't see any way I could make this cheat
work for this class, because every element of a data type needs to be
mapped with a different function.

You might want to take a look at the BNF-based size extension. Try

thm list.size
thm rose.size

to see what it has to offer. I suspect that you could base "count" on
"size_xxx" (e.g. "size_list"). If not, the idiom used to derive
"size"
systematically for all BNF-based datatypes might still serve as an
inspiration.

Thanks, I'll have a look. This doesn't seem to be in the Isabelle
2013-2 release, but I have no problem with switching to a repository
version.

The author of this entry is all in favor of porting it to the new
package, and it is, from what I understand, only a matter of time
until he gets to it. ;)

Well, in that case, here's one more person who'd like to see that
happening :-)

Cheers
Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Lars Hupel <hupel@in.tum.de>
Hi Florian,

unfortunately, this approach isn't modular. If I pull out the
specification of "count_rose" into a different constant, e.g.
"count_rose_pre", ideally I'd still want to use the instance "list ::
foo", but this requires the element type ("rose") to have a "foo"
instance. This naive translation merely trades a "circular constant
dependency" error message for a circular dependency which is impossible
to express.

Surely I can also pull out the definition of "count_list" and refer to
that, but my attempt failed:

datatype_new 'a seq = Cons 'a "'a seq" | Nil
datatype_new 'a rose = Fork 'a "'a rose seq"

primrec_new count_seq_pre where
"count_seq_pre _ Nil = 0" |
"count_seq_pre f (Cons x xs) = f x + count_seq_pre f xs"

primrec_new count_rose_pre where
"count_rose_pre f (Fork a as) = f a + count_seq_pre (count_rose_pre f)
as"

The error message is:

primrec_new error:
Invalid map function in "count_seq_pre (count_rose_pre f)"

If I change everything to "fun" and use "datatype_new_compat", the
function package is unable to find a termination order.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Lars,

Yes, I ran into this issue when implementing the "size" extension. To sort this out, it should be possible to rephrase the "primrec" specification so that it's expressed in terms of "map". Then you can derive the desired specification without "map" as a theorem. Perhaps we can discuss this live if you're in the office tomorrow.

Jasmin

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Dmitriy Traytel <traytel@in.tum.de>
If I understand it correctly, here really the same trick as for the size
function can be done: one uses two versions of the function:

s.t. "eval rs = eval_list rs (eval rs :: term => 'a :: evaluate => bool)"

For lists eval_list would be defined by:

primrec eval_list where
"eval_list rs ev t [] ⟷ rs ⊢ t ⟶* Const ''List.list.Nil''" |
"eval_list rs ev t (x # xs) ⟷ (∃t1 t2. ev t1 x ∧ eval_list rs ev t2 xs ∧
rs ⊢ t ⟶* Const ''List.list.Cons'' $ t1 $ t2)"

Then for rose trees:

datatype_new 'a tree = Node 'a "'a tree list"

primrec eval_tree where
"eval_tree rs ev u (Node a us) = (∃t ts. ev t a ∧
eval_list rs (λt f. f t) ts (map (λu t. eval_tree rs ev t u) us) ∧
rs ⊢ u ⟶* Const ''Scratch.tree.Node'' $ t $ ts)"

And the class instantiation again via

"eval rs = eval_tree rs (eval rs :: term => 'a :: evaluate => bool)"

Dmitriy

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Dmitriy Traytel <traytel@in.tum.de>
BTW: hopefully something like "eval_list rs (λt f. f t) ts (map (λu t.
eval_tree rs ev t u) us) = eval_list rs (eval_tree rs ev) ts us" will be
provable, such that one can get nice equations (similarly to what you
tried after Florian's suggestion hitting the syntactic restriction of
primrec).

Dmitriy

view this post on Zulip Email Gateway (Aug 19 2022 at 14:42):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Yet a few more thoughts.

To get a deeper understanding of the specification, you could try the
following:

a) provide a f corresponding to count ['a list] but abstracted over
count ['a] (»dictionary«)

b) define count ['a list] in terms of f

c) try to write down your specification for a g corresponding to count
['a rose].

If your specification mechanisms chokes then, its beyond the borders of
the specification mechanisms itself (at least in its particular setup).

If no, try to replace g by count ['a rose] using plain overloading
target (remove the const constraint from count if necessary). If this
is rejected, it is just not covered by overloaded definitions in Isabelle.

If no, the instantiation target itself cannot cover your specification.

Beyond that, I can emphasize what Jasmin has hinted at: particularly
concerning automatically derived specifications, you should not rely on
fun. For systematic instantiation, usually primrec specifications can
be achieved, perhaps including funny combinators defined once and for
all by hand.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 14:43):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Lars and all,

Indeed, currently everything in the AFP-entry Datatype_Order_Generator works via
the interface of the old datatype-package, but most of it is currently
accessible via datatype_compat (but not "derive countable").

It is on my TODO list to adapt the AFP-entry to the new datatype package, but
currently this is not a high-priority item, so it might take some while.

Cheers,
René

PS: I can only confirm Florian's comment on not using "fun" but primrec instead.
In the first version I tried to develop the order-generators via the function package
which turned out quite to be quite complicated / tedious. Once I switched to the
recursors from the old datatype package, the whole task became much simpler.
signature.asc

Last updated: Apr 30 2024 at 20:15 UTC