Email Gateway (Aug 22 2022 at 16:18): Email Gateway (Aug 22 2022 at 16:18):From: ducis <ducis_cn@126.com>
Hello,
I am trying to encapsulate matrices/vectors/arrays/lists as functions, similar to the matrices in
Gauss-Jordan Elimination for Matrices Represented as Functions, but without passing the dimensions
explicitly.
For example,
definition "l2f (xs::'a list) = (λ (i::nat) . xs ! i)"
value "let a = l2f [10,11,12,13::real] in a 1"
Is it possible to define some
"( nat => 'a ) => nat" (the size of the original list)
or
"( nat => 'a ) => (nat × nat) " or "( nat => 'a ) => nat set" (the domain of the function) ?
If it is impossible to define a computable one, is it possible to define an incomputable specifictaion?
Du
Email Gateway (Aug 22 2022 at 16:18):From: David Cock <david.cock@inf.ethz.ch>
Du,
The "function from indices to values" form throws away information,
so you've got to supply it back when you try to invert. There's no way
to extract the "length" of the original list from the function, as it's
got to be well defined for every possible index (functions in HOL are
total, even if the result isn't visibly defined). Your l2f function
returns some value a for any index i that you pass it.
One way of encoding the information you want might be a partial
function, that's only defined for those indices in the original list,
but that's likely to be less convenient to work with. Even then, you
need to "know" that the function came from a list in order to find the
length (to take, say, the largest index for which the output isn't None,
you'll need to supply a proof that there is such a maximum).
David
Last updated: Apr 20 2024 at 08:16 UTC