Email Gateway (Aug 19 2022 at 12:08): Email Gateway (Aug 19 2022 at 12:08):From: Tjark Weber <webertj@in.tum.de>
Hi,
There is a trick (due to John Harrison) to encode the dimension N of,
e.g., N-bit words with a type argument. The word libraries in
Isabelle/HOL and HOL4 are based on this approach.
In this setting, what is the recommended way to define a function that
performs recursion over N, i.e., whose result for an (N+1)-bit word is
naturally expressed in terms of its result for an N-bit word?
Best,
Tjark
Email Gateway (Aug 19 2022 at 12:09):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear Tjark,
I don't know how far the following solution is applicable to your
setting, but a somehow similar problem (and two different solutions)
were proposed in the mailing list by J. Harrison a while ago, for the
definition of determinants of matrices of dimension n, in terms of
determinants of matrices of size "n - 1":
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-January/msg00015.html
Hope it helps,
best,
Jesus
Email Gateway (Aug 19 2022 at 12:10):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Tjark,
I also think the general answer is no.
But maybe there is a trick (also called ugly hack) using type classes:
For a function "f" you want to define with primitive recursion on a type
"'a" you introduce a new type class:
class f_def =
fixes f :: "'a ⇒ nat"
Now you instantiate the option type (as the successor type):
instantiation option :: (f_def) f_def
begin
definition
"f_option (x::'a option) = f (undefined :: 'a) + 1"
instance ..
end
and one for the unit type (as termination)
instantiation unit :: f_def
begin
definition f_unit :: "unit ⇒ nat" where
"f_unit (x::unit) = 0"
instance ..
end
But a problem is that numeral types used by the word library and by
Multivariate Analysis use a binary representation instead of a unary
representation.
Email Gateway (Aug 19 2022 at 12:10):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Tjark and Johannes,
You can do recursion through such number types provided that you fix the representation of
numbers as types. The HOL-Word library does not fix the representation, but it uses a type
class (like f_def in Johannes' example), and AFAIK the same applies to
Multivariate_Analysis. It is merely the parser/pretty printer (in
HOL/Library/Numeral_Type) that translates numerals into type constructors, and this is
where the binary format comes from.
However, if you are sure that you will only ever need "primitive recursion" n -> n - 1,
then you can fix the representation to unary representations of sizes and do the
recursion. The following sketches the idea:
typedef 'a succ = "{0..<CARD('a)+1}" ...
consts f :: "'a :: len word => 'b :: len word"
defs (overloaded)
f_base: "f (x :: num1 word) = ..." -- "base case n = 1"
f_rec: "f (x :: 'a :: len succ word) = ... f (... :: 'a :: len word)"
Best,
Andreas
Last updated: Apr 19 2024 at 08:19 UTC