Stream: Beginner Questions

Topic: Easy way of expressing term size

Bob Rubbens (Apr 29 2023 at 15:20):

When dealing with custom termination proofs I tried using the "size" function, which counts the size of a datatype instance but not the things in it. I noticed this size function is also generated for each inductive type it seems? But then you need to supply a size function for the element type. This is okay but gets a bit annoying for nested types, such as nat list list. Is there also a version of "size_list" or maybe a typeclass that, pardon my naivety, does the obvious thing? So in this case I'd expect this naive_size function to also apply the proper size function for the inner type. So for the type nat list list, it would sum the sizes of all inner lists together, I think.

Bob Rubbens (Apr 29 2023 at 16:22):

Or maybe the following question is better: what's the idiomatic way to write down a decreases relation? What form should simp rules added to "termination_simp" have? (Because the way I'm writing them now, with "size" and "size_list size_some_type", they don't seem to compose very well with the termination proofs)

Manuel Eberl (May 06 2023 at 18:48):

I don't think something like this exists. I can see that it might be useful in some cases, but it does seem a bit ‘special purpose’. But I'm not an expert on datatypes, so it's possible that the thing you're looking for does exists somewhere and I just cannot find it.

You can create a typeclass of the form that you were suggesting quite easily, but of course you'll have to do all the instantiations by hand…

class full_size =
  fixes full_size :: "'a ⇒ nat"

instantiation nat :: full_size
begin
definition "full_size (n :: nat) = n"
instance ..
end

instantiation list :: (full_size) full_size
begin
definition "full_size = size_list full_size"
instance ..
end

value "full_size [1,2,3::nat]"

Bob Rubbens (May 06 2023 at 19:47):

That's too bad! I ended writing up small size functions for each of the datatypes where it mattered, e.g. "size_clause", "size_formula", etc. At least they were easy to write that way

Last updated: Dec 21 2024 at 16:20 UTC