Re: [isabelle] lift_definition + constructor



Andreas,

thanks for your kind offer ...

[...] You haven't mentioned code generation, but if you are interested, I'd be happy to explain the details.

... because code generation is in our focus: we want to generate algorithms from theories in algebraic geometry, while different algorithms require different representations of polynomials for efficiency reasons. So we are happy to hear ...

if you need pattern-matching only for code generation (e.g., to pick an efficient implementation), then that's still possible (to some extent) even if polynomials are not defined as a datatype.

... and in your paper [1] to find a quick guide to the following code snippets derived from [3]:

  datatype ('a, 'b) phantom = phantom 'b

  datatype poly_impl = Poly_IMPL
  definition poly_Recursive :: poly_impl where "poly_Recursive = Poly_IMPL"
definition poly_Distrib_Sparse :: poly_impl where "poly_Distrib_Sparse = Poly_IMPL" definition poly_Distrib_Sense :: poly_impl where "poly_Distrib_Sense = Poly_IMPL"

  class poly_impl =
    fixes poly_impl :: "('a, poly_impl) phantom"

  code_datatype poly_Recursive poly_Distrib_Sparse poly_Distrib_Sense

From now on we probably have to go another way: we need to choose different representations not specific with respect to types, but specific with respect to algorithms.

We are looking forward with great interest, how we can ...

* flexibly switch between representations of polynomials (probably even within one single, but complex algorithm) * derive properties for algorithms uniformly from a "logically unique representation for polynomials" like [2]

... and are going to study your approach in detail. Any hints are appreciated.

Walther

[1] http://www.infsec.ethz.ch/research/publications/pub2013/lochbihler13itp.pdf
[2] http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Polynomial.html
[3] http://afp.sourceforge.net/entries/Collections.shtml

On 12/16/2013 08:46 AM, Andreas Lochbihler wrote:
Walther,

Let me comment a bit, even though I am not an expert on polynomials in Isabelle. The definition in HOL/Library/Polynomials gives you a logically unique representation for polynomials, i.e., if two polynomials evaluate to the same at all points, then they are equal (in the sense of op =). Your construction with the datatype does not give you this identity, i.e., you get a different type with different properties. Of course, you can do so on your own, but in my experience redundancy in a type usually makes proving harder. Although you can interpret a polynomial in one representation or in the other, the logic does not distinguish them and neither can you in your proofs.

However, if you need pattern-matching only for code generation (e.g., to pick an efficient implementation), then that's still possible (to some extent) even if polynomials are not defined as a datatype.
Andreas
On 13/12/13 15:17, Walther Neuper wrote:
Brian,

thanks for your hints !
In the course of general considerations [1] we come back to this specific question:

On 11/19/2013 08:24 PM, Brian Huffman wrote:
On Tue, Nov 19, 2013 at 9:57 AM, Walther Neuper <wneuper at ist.tugraz.at> wrote:
In Isabelle2013-1 in HOL/Library/Polynomial there is

lift_definition pCons :: "'a::zero => 'a poly => 'a poly"
is "λa p. nat_case a (coeff p)"

Other kinds of representations, for instance sparse distributive polynomial representation like [2], could be lifted as well (establishing respective morphisms) by something like

    lift_definition dCons :: "..."
    is "..."


and then there is the question, how to distinguish between "pCons" and "dCons": pattern
matching, for instance by ...

    case p of
      pCons _ => ...
    | dCons _ => ...


... on constructors "pCons" and "dCons" was an idea ...

Is there a way to have a constructor "pCons" instead of function "pCons"?
I.e. a constructor like

datatype 'a pcons = Zero | pCons 'a "'a pcons"

could be somehow associated with lift_definition ? Or is this possible with
datatype_new ?
What exactly do you mean by "constructor"? HOL doesn't have any
built-in logical distinction between constructors and other functions.

The signatures of pCons, dCons, etc are under question, also the location with respect to the lift_definition --- do you find anything realisable about this idea ?

Walther

[1] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00262.html [2] http://afp.sourceforge.net/entries/Polynomials.shtml





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