Re: [isabelle] Recursion through Types



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

On 21/10/13 13:56, Johannes Hölzl wrote:

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.

  - Johannes


Am Sonntag, den 20.10.2013, 11:44 +0200 schrieb Jesus Aransay:
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


On Fri, Oct 18, 2013 at 7:29 PM, Tjark Weber <webertj at in.tum.de> wrote:
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














This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.