Email Gateway (Aug 18 2022 at 19:36): Email Gateway (Aug 18 2022 at 19:36):From: John Munroe <munddr@gmail.com>
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
Email Gateway (Aug 18 2022 at 19:36):From: Ramana Kumar <rk436@cam.ac.uk>
The type (real * real) would represent a point, not a graph.
You could represent a graph with (real * real) set, but you'd need to
additionally say that all the first components are distinct.
(real => real) seems a more suitable model.
Email Gateway (Aug 18 2022 at 19:36):From: Tjark Weber <webertj@in.tum.de>
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,
Tjark
Email Gateway (Aug 18 2022 at 19:37):From: Elsa L Gunter <egunter@illinois.edu>
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
Email Gateway (Aug 18 2022 at 19:37):From: Steven Obua <steven.obua@googlemail.com>
A further difference I have not seen mentioned so far is that in the set of pairs case, also the domain of the graph is encoded, whereas in the function representation the domain is essentially all of the reals.
Steven
Email Gateway (Aug 18 2022 at 19:37):From: Jens Doll <jd@cococo.de>
The (really) ambiguous word product has given me a lot of worthy
thoughts by now. We, or the mathematicians, see it as a combination of
two or more spaces. On the other hand I wonder which are the spaces a
real world product is made of? Look perhaps at my software product
Elbe, which consists of components from different vendors and
developers. Should I subsume it being simply a (cartesian) combination
of creative spaces?
Jens ;-)
BTW: There is a new version of Elbe and it is almost bug free:
https://cococo.de/Elbe/
Happy Reasoning!
Last updated: Nov 21 2024 at 12:39 UTC