Re: [isabelle] Product or function?

The type you use is somewhat dependent on your intended use. However, I should point out that something of type real * real is just a point in two dimensional space. The type of a graph in R^2 is (real * real) set, but that is also the type of any blob in R^2.

However you choose to model lines, you will need a type for the universe in which the line lives, and a predicate saying that the entity indeed is a line. If you chose to model a line as a set in R^2, then you could have a predicate

is_line L =
((\<forall> p \<in> L. fst p = (0::real)) \<and> (\<forall> y::real. \<exists> p\<in>L. snd p = y))
((\<exists> m. (\<forall> p1\<in> L. \<forall> p2\<in> L. ((snd p2 - snd p1) = m * (fst p2 - fst p1))))
 \<and> (\<forall> x. \<exists> p \<in> L. fst p = x))

If you chose to use functions, you would have to create a predicate expressing that it was linear (but then you would get totallity "for free"), but you would also have to deal with how you would represent the line
 y = 0.

There are other choices of base representation as well. For example, as the predicate is_line suggests, you might also want to consider sets of pairs of points, with a predicate describing that the set is exactly all the pairs of points witht he same ratio.

I suggest that you first think about to what uses you wish to put lines and let you base representation be guided by that.


On 4/26/12 12:31 AM, John Munroe wrote:

If I want to model a line graph, should I give it the type of a product
(real * real) or a function (real =>  real)? With a product type, would the
graph be perceived as a set of pairs?

Thanks for the help in advance.


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