Re: [isabelle] Multi-dimensional arrays

Am 30/04/2012 21:56, schrieb Aaron W. Hsu:
> Is there currently a theory for multi-dimensional arrays?  I have found 
> something called the Collections framework, but I do not know if this 
> fits the bill.  I am looking to create a theory based on the Mathematics 
> of Arrays, but if there was already a base for arrays, I would take that 
> as a starting point.

It depends on what you exactly want. The simplest way to model an array is as a
function  nat => 'a. A 2-dim array would have type  nat => nat => 'a. If you
want all arrays in the same type you could use  nat list => 'a. Of course these
models do not express that arrays have a fixed length. If you model arrays as
lists, that feature is captured as well. But arrays of different dimensions will
have different types, which may or may not bother you. This is the model in the
arrays of the collections framework, except that they wrap it up in a separate type.


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