# 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))
```\<or>
```
((\<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.
```
---Elsa

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

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.

John
```
```

```

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