plangeo5 http://www.win.tue.nl/~amc/oz/om/cds/plangeo5.ocd 2004-06-01 2006-06-01 0 2 experimental This CD contains symbols for generating polynomial systems from affine planar geometry configurations. coordinatize This symbol is a function of one argument which must be a configuration or an assertion (as defined in plangeo1). When applied to a configuration C, it stands for the same configuration but now with coordinates attached to each object of C. The new variables are bound within an OMBIND element with head element the lambda symbol. The bound variables (placed within an OMBVAR element) are the new variables, and the last argument of OMBIND is the expression C in which each object is coordinatized. If an object already has coordinates, these are left as they are. If not, then new variables are introduced to coordinatize the object. When applied to an assertion of the form assertion(C,S), it leads to the same result except that the last argument of OMBIND is the assertion whose configuration argument is the expression C in which each object is coordinatized, and whose thesis argument is S. The coordinatized version of the affine triangle with points A,B,C and lines a, b, c (through B and C, A and C, and A and B respectively) described in two ways: 1 1 1 1 0 1 1 1 1 1 0 The coordinatization of the assertion that two distinct lines meet in only one point is expressed as follows. It is equivalent to following expression. is_coordinatized This symbol is a boolean valued function of one argument which must be a configuration. When applied to an argument C, it represent the value true if C is a configuration such that each object occurring in C (as well as in its subconfigurations) has coordinates (that is, the set_affine_coordinates field is present as an argument to the object), and value false otherwise. If an object already has coordinates, these are left as they are. If not, then new variables are introduced to coordinatize the object. ideal This symbol is a function in one argument, which should be a coordinatized configuration (that is, each geometric object involved has coordinates). When evaluated at a configuration C it represents a function (given by a lambda binder) mapping the new parameters (arising when the inequality properties in the configuration are being translated into polynomials) to a list of polynomials in the coordinates that are variables which, when equated to zero, represent conditions equivalent to those describing the configuration C. When evaluated at an assertion assertion(C,S) it represents a function (given by a lambda binder) mapping the new parameters (arising when the inequality properties in the configuration are being translated into polynomials) to a list of polynomials in the coordinates that are variables which, when equated to zero, represent conditions equivalent to those describing the configuration C. The following expression is an ideal of a coordinatized triangle. 1 1 1 1 0 Its evaluation should be equivalent to -1 polynomial_assertion This symbol is a function in one argument, which should be an assertion whose configuration is coordinatized (that is, each geometric object involved has coordinates). When evaluated at an assertion assertion(C,T) it represents the assertion that the constant polynomial 1 belongs to the ideal of the polynomial ring over a coefficient ring R containing the rationals and all global (unbound) coordinates of C, in the bound variables of ideal(C) and an external variable t, generated by ideal(C)[bound variables] and 1-f_T t. Here f_T is a polynomial such that f_T=0 is equivalent to the thesis T being true. This means f_T is in the radical ideal of ideal(C)[bound variables]. The interpretation is as follows: There are no parameter choices for the bound variables such that f_T is nonzero. In other words, for all parameter choices of a coordinatization of C, we must have f_T=0. So the truth of the assertion that thesis T holds in configuration C is reflected by the truth of polynomial_assertion(C,T).