Re: [isabelle] Product or function?

On Thu, 2012-04-26 at 06:31 +0100, 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?

A line is often defined as a set of points (whose coordinates satisfy a
linear equation). The corresponding HOL type would be (a subtype of)
"(real * real) set".

The type "real => real" of real-valued functions is both too general (as
it also contains non-linear functions) and too restrictive (as it does
not contain lines that are parallel to the y-axis).

However, there are many different ways to *describe* a straight line:
for instance, via two distinct points (corresponding to (a subtype of)
"(real * real) * (real * real)"), or via a linear equation of the form
ax+by=c, where ab <> 0 (corresponding to (a subtype of) "real * real *
real"). It is difficult to give more specific advice without knowing
your application.

Best regards,

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