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
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