Canonical URL:

http://www.win.tue.nl/~amc/oz/om/cds/plangeo5.ocd

CD Base:

http://www.openmath.org/cd

CD File:

plangeo5.ocd

CD as XML Encoded OpenMath:

plangeo5.omcd

Defines:

coordinatize, ideal, is_coordinatized, polynomial_assertion

Date:

2004-06-01

Version:

0 (Revision 2)

Review Date:

2006-06-01

Status:

experimental

This CD contains symbols for generating polynomial systems from affine planar geometry configurations.

coordinatize

Description:

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.

Example:

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:

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="plangeo5" name="coordinatize"/>
    <OMA><OMS cd="plangeo1" name="configuration"/>
      <OMA><OMS cd="plangeo1" name="point"/>
        <OMV name="A"/>
      </OMA>
      <OMA><OMS cd="plangeo1" name="point"/>
        <OMV name="B"/>
      </OMA>
      <OMA><OMS cd="plangeo1" name="line"/>
        <OMV name="c"/>
        <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
          <OMV name="c"/>
          <OMA><OMS cd="linalg2" name="vector"/>
            <OMI>1</OMI>
            <OMI>1</OMI>
            <OMI>1</OMI>
          </OMA>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="c"/>
          <OMV name="A"/>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="c"/>
          <OMV name="B"/>
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="point"/>
        <OMV name="C"/>
        <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
          <OMV name="C"/>
          <OMA><OMS cd="linalg2" name="vector"/>
            <OMI>1</OMI>
            <OMI>0</OMI>
            <OMI>1</OMI>
          </OMA>
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="line"/>
       <OMV name="a"/>
       <OMA><OMS cd="plangeo1" name="incident"/>
         <OMV name="a"/>
         <OMV name="B"/>
       </OMA>
       <OMA><OMS cd="plangeo1" name="incident"/>
         <OMV name="a"/>
         <OMV name="C"/>
       </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="line"/>
        <OMV name="b"/>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="b"/>
          <OMV name="A"/>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="b"/>
          <OMV name="C"/>
        </OMA>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo5">coordinatize</csymbol>
  <apply><csymbol cd="plangeo1">configuration</csymbol>
   <apply><csymbol cd="plangeo1">point</csymbol><ci>A</ci></apply>
   <apply><csymbol cd="plangeo1">point</csymbol><ci>B</ci></apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>c</ci>
    <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
     <ci>c</ci>
     <apply><csymbol cd="linalg2">vector</csymbol>
      <cn type="integer">1</cn>
      <cn type="integer">1</cn>
      <cn type="integer">1</cn>
     </apply>
    </apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>c</ci><ci>A</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>c</ci><ci>B</ci></apply>
   </apply>
   <apply><csymbol cd="plangeo1">point</csymbol>
    <ci>C</ci>
    <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
     <ci>C</ci>
     <apply><csymbol cd="linalg2">vector</csymbol>
      <cn type="integer">1</cn>
      <cn type="integer">0</cn>
      <cn type="integer">1</cn>
     </apply>
    </apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>a</ci>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>a</ci><ci>B</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>a</ci><ci>C</ci></apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>b</ci>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>b</ci><ci>A</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>b</ci><ci>C</ci></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

coordinatize (configuration (point ( A) , point ( B) , line ( c, set_affine_coordinates ( c, vector (1, 1, 1) ) , incident ( c, A) , incident ( c, B) ) , point ( C, set_affine_coordinates ( C, vector (1, 0, 1) ) ) , line ( a, incident ( a, B) , incident ( a, C) ) , line ( b, incident ( b, A) , incident ( b, C) ) ) )

Popcorn

plangeo5.coordinatize(plangeo1.configuration(plangeo1.point($A), plangeo1.point($B), plangeo1.line($c, plangeo4.set_affine_coordinates($c, linalg2.vector(1, 1, 1)), plangeo1.incident($c, $A), plangeo1.incident($c, $B)), plangeo1.point($C, plangeo4.set_affine_coordinates($C, linalg2.vector(1, 0, 1))), plangeo1.line($a, plangeo1.incident($a, $B), plangeo1.incident($a, $C)), plangeo1.line($b, plangeo1.incident($b, $A), plangeo1.incident($b, $C))))

Rendered Presentation MathML

$$\mathrm{coordinatize}\left(\mathrm{configuration}(\mathrm{point}\left(A\right),\mathrm{point}\left(B\right),\mathrm{line}(c,\mathrm{set\_affine\_coordinates}(c,(1,1,1)),\mathrm{incident}(c,A),\mathrm{incident}(c,B)),\mathrm{point}(C,\mathrm{set\_affine\_coordinates}(C,(1,0,1))),\mathrm{line}(a,\mathrm{incident}(a,B),\mathrm{incident}(a,C)),\mathrm{line}(b,\mathrm{incident}(b,A),\mathrm{incident}(b,C)))\right)$$

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMBIND><OMS cd="fns1" name="lambda"/>
    <OMBVAR>
            <OMV name="xA"/>
            <OMV name="yA"/>
            <OMV name="xB"/>
            <OMV name="yB"/>
            <OMV name="xa"/>
            <OMV name="ya"/>          
            <OMV name="za"/>
            <OMV name="xb"/>
            <OMV name="yb"/>
            <OMV name="zb"/>          
    </OMBVAR>
    <OMA><OMS cd="plangeo1" name="configuration"/>
      <OMA><OMS cd="plangeo1" name="point"/>
        <OMV name="A"/>
        <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
          <OMV name="A"/>
          <OMA><OMS cd="linalg2" name="vector"/>
            <OMV name="xA"/>
            <OMV name="yA"/>
          </OMA>
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="point"/>
        <OMV name="B"/>
        <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
          <OMV name="B"/>
          <OMA><OMS cd="linalg2" name="vector"/>
            <OMV name="xB"/>
            <OMV name="yB"/>
          </OMA>
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="line"/>
        <OMV name="c"/>
        <OMA><OMS cd="plangeo4" name="set_coordinates"/>
          <OMV name="c"/>
          <OMA><OMS cd="linalg2" name="vector"/>
            <OMI>1</OMI>
            <OMI>1</OMI>
            <OMI>1</OMI>
          </OMA>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="c"/>
          <OMV name="A"/>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="c"/>
          <OMV name="B"/>
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="point"/>
        <OMV name="C"/>
        <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
          <OMV name="C"/>
          <OMA><OMS cd="linalg2" name="vector"/>
            <OMI>1</OMI>
            <OMI>0</OMI>
          </OMA>
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="line"/>
        <OMV name="a"/>
        <OMA><OMS cd="plangeo4" name="set_coordinates"/>
          <OMV name="a"/>
          <OMA><OMS cd="linalg2" name="vector"/>
            <OMV name="xa"/>
            <OMV name="ya"/>          
            <OMV name="za"/>          
          </OMA>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="a"/>
          <OMV name="B"/>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="a"/>
          <OMV name="C"/>
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="line"/>
        <OMV name="b"/>
        <OMA><OMS cd="plangeo4" name="set_coordinates"/>
          <OMV name="b"/>
          <OMA><OMS cd="linalg2" name="vector"/>
            <OMV name="xb"/>
            <OMV name="yb"/>          
            <OMV name="zb"/>          
          </OMA>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="b"/>
          <OMV name="A"/>
        </OMA>
        <OMA><OMS cd="plangeo1" name="incident"/>
          <OMV name="b"/>
          <OMV name="C"/>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="fns1">lambda</csymbol>
  <bvar><ci>xA</ci></bvar>
  <bvar><ci>yA</ci></bvar>
  <bvar><ci>xB</ci></bvar>
  <bvar><ci>yB</ci></bvar>
  <bvar><ci>xa</ci></bvar>
  <bvar><ci>ya</ci></bvar>
  <bvar><ci>za</ci></bvar>
  <bvar><ci>xb</ci></bvar>
  <bvar><ci>yb</ci></bvar>
  <bvar><ci>zb</ci></bvar>
  <apply><csymbol cd="plangeo1">configuration</csymbol>
   <apply><csymbol cd="plangeo1">point</csymbol>
    <ci>A</ci>
    <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
     <ci>A</ci>
     <apply><csymbol cd="linalg2">vector</csymbol><ci>xA</ci><ci>yA</ci></apply>
    </apply>
   </apply>
   <apply><csymbol cd="plangeo1">point</csymbol>
    <ci>B</ci>
    <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
     <ci>B</ci>
     <apply><csymbol cd="linalg2">vector</csymbol><ci>xB</ci><ci>yB</ci></apply>
    </apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>c</ci>
    <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
     <ci>c</ci>
     <apply><csymbol cd="linalg2">vector</csymbol>
      <cn type="integer">1</cn>
      <cn type="integer">1</cn>
      <cn type="integer">1</cn>
     </apply>
    </apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>c</ci><ci>A</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>c</ci><ci>B</ci></apply>
   </apply>
   <apply><csymbol cd="plangeo1">point</csymbol>
    <ci>C</ci>
    <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
     <ci>C</ci>
     <apply><csymbol cd="linalg2">vector</csymbol>
      <cn type="integer">1</cn>
      <cn type="integer">0</cn>
     </apply>
    </apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>a</ci>
    <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="linalg2">vector</csymbol><ci>xa</ci><ci>ya</ci><ci>za</ci></apply>
    </apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>a</ci><ci>B</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>a</ci><ci>C</ci></apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>b</ci>
    <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
     <ci>b</ci>
     <apply><csymbol cd="linalg2">vector</csymbol><ci>xb</ci><ci>yb</ci><ci>zb</ci></apply>
    </apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>b</ci><ci>A</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>b</ci><ci>C</ci></apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

lambda [ xA yA xB yB xa ya za xb yb zb ] . (configuration (point ( A, set_affine_coordinates ( A, vector ( xA, yA) ) ) , point ( B, set_affine_coordinates ( B, vector ( xB, yB) ) ) , line ( c, set_coordinates ( c, vector (1, 1, 1) ) , incident ( c, A) , incident ( c, B) ) , point ( C, set_affine_coordinates ( C, vector (1, 0) ) ) , line ( a, set_coordinates ( a, vector ( xa, ya, za) ) , incident ( a, B) , incident ( a, C) ) , line ( b, set_coordinates ( b, vector ( xb, yb, zb) ) , incident ( b, A) , incident ( b, C) ) ) )

Popcorn

fns1.lambda[$xA, $yA, $xB, $yB, $xa, $ya, $za, $xb, $yb, $zb -> plangeo1.configuration(plangeo1.point($A, plangeo4.set_affine_coordinates($A, linalg2.vector($xA, $yA))), plangeo1.point($B, plangeo4.set_affine_coordinates($B, linalg2.vector($xB, $yB))), plangeo1.line($c, plangeo4.set_coordinates($c, linalg2.vector(1, 1, 1)), plangeo1.incident($c, $A), plangeo1.incident($c, $B)), plangeo1.point($C, plangeo4.set_affine_coordinates($C, linalg2.vector(1, 0))), plangeo1.line($a, plangeo4.set_coordinates($a, linalg2.vector($xa, $ya, $za)), plangeo1.incident($a, $B), plangeo1.incident($a, $C)), plangeo1.line($b, plangeo4.set_coordinates($b, linalg2.vector($xb, $yb, $zb)), plangeo1.incident($b, $A), plangeo1.incident($b, $C)))]

Rendered Presentation MathML

$$\lambda \hspace{0.17em}\mathrm{xA},\mathrm{yA},\mathrm{xB},\mathrm{yB},\mathrm{xa},\mathrm{ya},\mathrm{za},\mathrm{xb},\mathrm{yb},\mathrm{zb}.\mathrm{configuration}(\mathrm{point}(A,\mathrm{set\_affine\_coordinates}(A,(\mathrm{xA},\mathrm{yA}))),\mathrm{point}(B,\mathrm{set\_affine\_coordinates}(B,(\mathrm{xB},\mathrm{yB}))),\mathrm{line}(c,\mathrm{set\_coordinates}(c,(1,1,1)),\mathrm{incident}(c,A),\mathrm{incident}(c,B)),\mathrm{point}(C,\mathrm{set\_affine\_coordinates}(C,(1,0))),\mathrm{line}(a,\mathrm{set\_coordinates}(a,(\mathrm{xa},\mathrm{ya},\mathrm{za})),\mathrm{incident}(a,B),\mathrm{incident}(a,C)),\mathrm{line}(b,\mathrm{set\_coordinates}(b,(\mathrm{xb},\mathrm{yb},\mathrm{zb})),\mathrm{incident}(b,A),\mathrm{incident}(b,C)))$$

Example:

The coordinatization of the assertion that two distinct lines meet in only one point is expressed as follows.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="plangeo5" name="coordinatize"/>
     <OMA><OMS cd="plangeo1" name="assertion"/>
          <OMA><OMS cd="plangeo1" name="configuration"/>
               <OMA><OMS cd="plangeo1" name="point"/> 
                    <OMV name="A"/>
               </OMA>
               <OMA><OMS cd="plangeo1" name="point"/> 
                    <OMV name="B"/>
               </OMA>
               <OMA><OMS cd="plangeo1" name="line"/>
                    <OMV name="l"/>
                    <OMA><OMS cd="plangeo1" name="incident"/>
                         <OMV name="A"/>
                         <OMV name="l"/>
                    </OMA>
                    <OMA><OMS cd="plangeo1" name="incident"/>
                         <OMV name="B"/>
                         <OMV name="l"/>
                    </OMA>
               </OMA>
               <OMA><OMS cd="plangeo1" name="line"/>
                    <OMV name="m"/>
                    <OMA><OMS cd="plangeo1" name="incident"/>
                         <OMV name="A"/>
                         <OMV name="m"/>
                    </OMA>
                    <OMA><OMS cd="plangeo1" name="incident"/>
                         <OMV name="B"/>
                         <OMV name="m"/>
                    </OMA>
                    <OMA><OMS cd="logic1" name="not"/>
                         <OMA><OMS cd="relation1" name="eq"/>
                              <OMV name="l"/>
                              <OMV name="m"/>
                         </OMA>
                    </OMA>
               </OMA>
               <OMA><OMS cd="relation1" name="eq"/>
                    <OMV name="A"/>
                    <OMV name="B"/>
               </OMA>
          </OMA>
     </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo5">coordinatize</csymbol>
  <apply><csymbol cd="plangeo1">assertion</csymbol>
   <apply><csymbol cd="plangeo1">configuration</csymbol>
    <apply><csymbol cd="plangeo1">point</csymbol><ci>A</ci></apply>
    <apply><csymbol cd="plangeo1">point</csymbol><ci>B</ci></apply>
    <apply><csymbol cd="plangeo1">line</csymbol>
     <ci>l</ci>
     <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>l</ci></apply>
     <apply><csymbol cd="plangeo1">incident</csymbol><ci>B</ci><ci>l</ci></apply>
    </apply>
    <apply><csymbol cd="plangeo1">line</csymbol>
     <ci>m</ci>
     <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>m</ci></apply>
     <apply><csymbol cd="plangeo1">incident</csymbol><ci>B</ci><ci>m</ci></apply>
     <apply><csymbol cd="logic1">not</csymbol>
      <apply><csymbol cd="relation1">eq</csymbol><ci>l</ci><ci>m</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol><ci>A</ci><ci>B</ci></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

coordinatize (assertion (configuration (point ( A) , point ( B) , line ( l, incident ( A, l) , incident ( B, l) ) , line ( m, incident ( A, m) , incident ( B, m) , not (eq ( l, m) ) ) , eq ( A, B) ) ) )

Popcorn

plangeo5.coordinatize(plangeo1.assertion(plangeo1.configuration(plangeo1.point($A), plangeo1.point($B), plangeo1.line($l, plangeo1.incident($A, $l), plangeo1.incident($B, $l)), plangeo1.line($m, plangeo1.incident($A, $m), plangeo1.incident($B, $m), not($l = $m)), $A = $B)))

Rendered Presentation MathML

$$\mathrm{coordinatize}\left(\mathrm{assertion}\left(\mathrm{configuration}(\mathrm{point}\left(A\right),\mathrm{point}\left(B\right),\mathrm{line}(l,\mathrm{incident}(A,l),\mathrm{incident}(B,l)),\mathrm{line}(m,\mathrm{incident}(A,m),\mathrm{incident}(B,m),\neg (l=m)),A=B)\right)\right)$$

It is equivalent to following expression.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMBIND><OMS cd="fns1" name="lambda"/>
<OMBVAR><OMV name="xA"/><OMV name="yA"/>
        <OMV name="xB"/><OMV name="yB"/>
        <OMV name="xl"/><OMV name="yl"/><OMV name="zl"/>
        <OMV name="xm"/><OMV name="ym"/><OMV name="zm"/>
</OMBVAR>
<OMA><OMS cd="plangeo1" name="assertion"/>
     <OMA><OMS cd="plangeo1" name="configuration"/>
          <OMA><OMS cd="plangeo1" name="point"/> 
               <OMV name="A"/>
               <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
                    <OMV name="A"/>
                    <OMA><OMS cd="linalg2" name="vector"/>
                         <OMV name="xA"/>
                         <OMV name="yA"/>
                    </OMA>
               </OMA>
          </OMA>
          <OMA><OMS cd="plangeo1" name="point"/> 
               <OMV name="B"/>
               <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
                    <OMV name="B"/>
                    <OMA><OMS cd="linalg2" name="vector"/>
                         <OMV name="xB"/>
                         <OMV name="yB"/>
                    </OMA>
               </OMA>

          </OMA>
          <OMA><OMS cd="plangeo1" name="line"/>
               <OMV name="l"/>
               <OMA><OMS cd="plangeo1" name="incident"/>
                    <OMV name="A"/>
                    <OMV name="l"/>
               </OMA>
               <OMA><OMS cd="plangeo1" name="incident"/>
                    <OMV name="B"/>
                    <OMV name="l"/>
               </OMA>
               <OMA><OMS cd="plangeo4" name="set_coordinates"/>
                    <OMV name="l"/>
                    <OMA><OMS cd="linalg2" name="vector"/>
                         <OMV name="xl"/><OMV name="yl"/><OMV name="zl"/>
                    </OMA>
               </OMA>

          </OMA>
          <OMA><OMS cd="plangeo1" name="line"/>
               <OMV name="m"/>
               <OMA><OMS cd="plangeo1" name="incident"/>
                    <OMV name="A"/>
                    <OMV name="m"/>
               </OMA>
               <OMA><OMS cd="plangeo1" name="incident"/>
                    <OMV name="B"/>
                    <OMV name="m"/>
               </OMA>
               <OMA><OMS cd="logic1" name="not"/>
                    <OMA><OMS cd="relation1" name="eq"/>
                         <OMV name="l"/>
                         <OMV name="m"/>
                    </OMA>
               </OMA>
               <OMA><OMS cd="plangeo4" name="set_coordinates"/>
                    <OMV name="m"/>
                    <OMA><OMS cd="linalg2" name="vector"/>
                         <OMV name="xm"/> <OMV name="ym"/><OMV name="zm"/>
                    </OMA>
               </OMA>
          </OMA>
          <OMA><OMS cd="relation1" name="eq"/>
               <OMV name="A"/>
               <OMV name="B"/>
          </OMA>
     </OMA>
</OMA>
</OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="fns1">lambda</csymbol>
  <bvar><ci>xA</ci></bvar>
  <bvar><ci>yA</ci></bvar>
  <bvar><ci>xB</ci></bvar>
  <bvar><ci>yB</ci></bvar>
  <bvar><ci>xl</ci></bvar>
  <bvar><ci>yl</ci></bvar>
  <bvar><ci>zl</ci></bvar>
  <bvar><ci>xm</ci></bvar>
  <bvar><ci>ym</ci></bvar>
  <bvar><ci>zm</ci></bvar>
  <apply><csymbol cd="plangeo1">assertion</csymbol>
   <apply><csymbol cd="plangeo1">configuration</csymbol>
    <apply><csymbol cd="plangeo1">point</csymbol>
     <ci>A</ci>
     <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
      <ci>A</ci>
      <apply><csymbol cd="linalg2">vector</csymbol><ci>xA</ci><ci>yA</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="plangeo1">point</csymbol>
     <ci>B</ci>
     <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
      <ci>B</ci>
      <apply><csymbol cd="linalg2">vector</csymbol><ci>xB</ci><ci>yB</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="plangeo1">line</csymbol>
     <ci>l</ci>
     <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>l</ci></apply>
     <apply><csymbol cd="plangeo1">incident</csymbol><ci>B</ci><ci>l</ci></apply>
     <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
      <ci>l</ci>
      <apply><csymbol cd="linalg2">vector</csymbol><ci>xl</ci><ci>yl</ci><ci>zl</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="plangeo1">line</csymbol>
     <ci>m</ci>
     <apply><csymbol cd="plangeo1">incident</csymbol><ci>A</ci><ci>m</ci></apply>
     <apply><csymbol cd="plangeo1">incident</csymbol><ci>B</ci><ci>m</ci></apply>
     <apply><csymbol cd="logic1">not</csymbol>
      <apply><csymbol cd="relation1">eq</csymbol><ci>l</ci><ci>m</ci></apply>
     </apply>
     <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
      <ci>m</ci>
      <apply><csymbol cd="linalg2">vector</csymbol><ci>xm</ci><ci>ym</ci><ci>zm</ci></apply>
     </apply>
    </apply>
    <apply><csymbol cd="relation1">eq</csymbol><ci>A</ci><ci>B</ci></apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

lambda [ xA yA xB yB xl yl zl xm ym zm ] . (assertion (configuration (point ( A, set_affine_coordinates ( A, vector ( xA, yA) ) ) , point ( B, set_affine_coordinates ( B, vector ( xB, yB) ) ) , line ( l, incident ( A, l) , incident ( B, l) , set_coordinates ( l, vector ( xl, yl, zl) ) ) , line ( m, incident ( A, m) , incident ( B, m) , not (eq ( l, m) ) , set_coordinates ( m, vector ( xm, ym, zm) ) ) , eq ( A, B) ) ) )

Popcorn

fns1.lambda[$xA, $yA, $xB, $yB, $xl, $yl, $zl, $xm, $ym, $zm -> plangeo1.assertion(plangeo1.configuration(plangeo1.point($A, plangeo4.set_affine_coordinates($A, linalg2.vector($xA, $yA))), plangeo1.point($B, plangeo4.set_affine_coordinates($B, linalg2.vector($xB, $yB))), plangeo1.line($l, plangeo1.incident($A, $l), plangeo1.incident($B, $l), plangeo4.set_coordinates($l, linalg2.vector($xl, $yl, $zl))), plangeo1.line($m, plangeo1.incident($A, $m), plangeo1.incident($B, $m), not($l = $m), plangeo4.set_coordinates($m, linalg2.vector($xm, $ym, $zm))), $A = $B))]

Rendered Presentation MathML

$$\lambda \hspace{0.17em}\mathrm{xA},\mathrm{yA},\mathrm{xB},\mathrm{yB},\mathrm{xl},\mathrm{yl},\mathrm{zl},\mathrm{xm},\mathrm{ym},\mathrm{zm}.\mathrm{assertion}\left(\mathrm{configuration}(\mathrm{point}(A,\mathrm{set\_affine\_coordinates}(A,(\mathrm{xA},\mathrm{yA}))),\mathrm{point}(B,\mathrm{set\_affine\_coordinates}(B,(\mathrm{xB},\mathrm{yB}))),\mathrm{line}(l,\mathrm{incident}(A,l),\mathrm{incident}(B,l),\mathrm{set\_coordinates}(l,(\mathrm{xl},\mathrm{yl},\mathrm{zl}))),\mathrm{line}(m,\mathrm{incident}(A,m),\mathrm{incident}(B,m),\neg (l=m),\mathrm{set\_coordinates}(m,(\mathrm{xm},\mathrm{ym},\mathrm{zm}))),A=B)\right)$$

Signatures:

sts

is_coordinatized

Description:

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.

Signatures:

sts

ideal

Description:

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.

Example:

The following expression is an ideal of a coordinatized triangle.

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="plangeo5" name="ideal"/>
  <OMA><OMS cd="plangeo1" name="configuration"/>
    <OMA><OMS cd="plangeo1" name="point"/>
      <OMV name="A"/>
      <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
        <OMV name="A"/>
        <OMA><OMS cd="linalg2" name="vector"/>
          <OMV name="xA"/>
          <OMV name="yA"/>
        </OMA>
      </OMA>
    </OMA>
    <OMA><OMS cd="plangeo1" name="point"/>
      <OMV name="B"/>
      <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
        <OMV name="B"/>
        <OMA><OMS cd="linalg2" name="vector"/>
          <OMV name="xB"/>
          <OMV name="yB"/>
        </OMA>
      </OMA>
      <OMA><OMS cd="logic1" name="not"/>
        <OMA><OMS cd="relation1" name="eq"/>
          <OMV name="B"/>
          <OMV name="A"/>
        </OMA>
      </OMA>
    </OMA>
    <OMA><OMS cd="plangeo1" name="line"/>
      <OMV name="c"/>
      <OMA><OMS cd="plangeo4" name="set_coordinates"/>
        <OMV name="c"/>
        <OMA><OMS cd="linalg2" name="vector"/>
          <OMI>1</OMI>
          <OMI>1</OMI>
          <OMI>1</OMI>
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="incident"/>
        <OMV name="c"/>
        <OMV name="A"/>
      </OMA>
      <OMA><OMS cd="plangeo1" name="incident"/>
        <OMV name="c"/>
        <OMV name="B"/>
      </OMA>
    </OMA>
    <OMA><OMS cd="plangeo1" name="point"/>
      <OMV name="C"/>
      <OMA><OMS cd="plangeo4" name="set_affine_coordinates"/>
        <OMV name="C"/>
        <OMA><OMS cd="linalg2" name="vector"/>
          <OMI>1</OMI>
          <OMI>0</OMI>
        </OMA>
      </OMA>
    </OMA>
    <OMA><OMS cd="plangeo1" name="line"/>
      <OMV name="a"/>
      <OMA><OMS cd="plangeo4" name="set_coordinates"/>
        <OMV name="a"/>
        <OMA><OMS cd="linalg2" name="vector"/>
          <OMV name="xa"/><OMV name="ya"/><OMV name="za"/>          
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="incident"/>
        <OMV name="a"/>
        <OMV name="B"/>
      </OMA>
      <OMA><OMS cd="plangeo1" name="incident"/>
        <OMV name="a"/>
        <OMV name="C"/>
      </OMA>
    </OMA>
    <OMA><OMS cd="plangeo1" name="line"/>
      <OMV name="b"/>
      <OMA><OMS cd="plangeo4" name="set_coordinates"/>
        <OMV name="b"/>
        <OMA><OMS cd="linalg2" name="vector"/>
          <OMV name="xb"/><OMV name="yb"/><OMV name="zb"/>          
        </OMA>
      </OMA>
      <OMA><OMS cd="plangeo1" name="incident"/>
        <OMV name="b"/>
        <OMV name="A"/>
      </OMA>
      <OMA><OMS cd="plangeo1" name="incident"/>
        <OMV name="b"/>
        <OMV name="C"/>
      </OMA>
    </OMA>
  </OMA>
</OMA>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <apply><csymbol cd="plangeo5">ideal</csymbol>
  <apply><csymbol cd="plangeo1">configuration</csymbol>
   <apply><csymbol cd="plangeo1">point</csymbol>
    <ci>A</ci>
    <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
     <ci>A</ci>
     <apply><csymbol cd="linalg2">vector</csymbol><ci>xA</ci><ci>yA</ci></apply>
    </apply>
   </apply>
   <apply><csymbol cd="plangeo1">point</csymbol>
    <ci>B</ci>
    <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
     <ci>B</ci>
     <apply><csymbol cd="linalg2">vector</csymbol><ci>xB</ci><ci>yB</ci></apply>
    </apply>
    <apply><csymbol cd="logic1">not</csymbol>
     <apply><csymbol cd="relation1">eq</csymbol><ci>B</ci><ci>A</ci></apply>
    </apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>c</ci>
    <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
     <ci>c</ci>
     <apply><csymbol cd="linalg2">vector</csymbol>
      <cn type="integer">1</cn>
      <cn type="integer">1</cn>
      <cn type="integer">1</cn>
     </apply>
    </apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>c</ci><ci>A</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>c</ci><ci>B</ci></apply>
   </apply>
   <apply><csymbol cd="plangeo1">point</csymbol>
    <ci>C</ci>
    <apply><csymbol cd="plangeo4">set_affine_coordinates</csymbol>
     <ci>C</ci>
     <apply><csymbol cd="linalg2">vector</csymbol>
      <cn type="integer">1</cn>
      <cn type="integer">0</cn>
     </apply>
    </apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>a</ci>
    <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
     <ci>a</ci>
     <apply><csymbol cd="linalg2">vector</csymbol><ci>xa</ci><ci>ya</ci><ci>za</ci></apply>
    </apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>a</ci><ci>B</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>a</ci><ci>C</ci></apply>
   </apply>
   <apply><csymbol cd="plangeo1">line</csymbol>
    <ci>b</ci>
    <apply><csymbol cd="plangeo4">set_coordinates</csymbol>
     <ci>b</ci>
     <apply><csymbol cd="linalg2">vector</csymbol><ci>xb</ci><ci>yb</ci><ci>zb</ci></apply>
    </apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>b</ci><ci>A</ci></apply>
    <apply><csymbol cd="plangeo1">incident</csymbol><ci>b</ci><ci>C</ci></apply>
   </apply>
  </apply>
 </apply>
</math>

Prefix

ideal (configuration (point ( A, set_affine_coordinates ( A, vector ( xA, yA) ) ) , point ( B, set_affine_coordinates ( B, vector ( xB, yB) ) , not (eq ( B, A) ) ) , line ( c, set_coordinates ( c, vector (1, 1, 1) ) , incident ( c, A) , incident ( c, B) ) , point ( C, set_affine_coordinates ( C, vector (1, 0) ) ) , line ( a, set_coordinates ( a, vector ( xa, ya, za) ) , incident ( a, B) , incident ( a, C) ) , line ( b, set_coordinates ( b, vector ( xb, yb, zb) ) , incident ( b, A) , incident ( b, C) ) ) )

Popcorn

plangeo5.ideal(plangeo1.configuration(plangeo1.point($A, plangeo4.set_affine_coordinates($A, linalg2.vector($xA, $yA))), plangeo1.point($B, plangeo4.set_affine_coordinates($B, linalg2.vector($xB, $yB)), not($B = $A)), plangeo1.line($c, plangeo4.set_coordinates($c, linalg2.vector(1, 1, 1)), plangeo1.incident($c, $A), plangeo1.incident($c, $B)), plangeo1.point($C, plangeo4.set_affine_coordinates($C, linalg2.vector(1, 0))), plangeo1.line($a, plangeo4.set_coordinates($a, linalg2.vector($xa, $ya, $za)), plangeo1.incident($a, $B), plangeo1.incident($a, $C)), plangeo1.line($b, plangeo4.set_coordinates($b, linalg2.vector($xb, $yb, $zb)), plangeo1.incident($b, $A), plangeo1.incident($b, $C))))

Rendered Presentation MathML

$$\mathrm{ideal}\left(\mathrm{configuration}(\mathrm{point}(A,\mathrm{set\_affine\_coordinates}(A,(\mathrm{xA},\mathrm{yA}))),\mathrm{point}(B,\mathrm{set\_affine\_coordinates}(B,(\mathrm{xB},\mathrm{yB})),\neg (B=A)),\mathrm{line}(c,\mathrm{set\_coordinates}(c,(1,1,1)),\mathrm{incident}(c,A),\mathrm{incident}(c,B)),\mathrm{point}(C,\mathrm{set\_affine\_coordinates}(C,(1,0))),\mathrm{line}(a,\mathrm{set\_coordinates}(a,(\mathrm{xa},\mathrm{ya},\mathrm{za})),\mathrm{incident}(a,B),\mathrm{incident}(a,C)),\mathrm{line}(b,\mathrm{set\_coordinates}(b,(\mathrm{xb},\mathrm{yb},\mathrm{zb})),\mathrm{incident}(b,A),\mathrm{incident}(b,C)))\right)$$

Its evaluation should be equivalent to

OpenMath XML (source)

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMBIND><OMS cd="fns1" name="lambda"/>
    <OMBVAR>
            <OMV name="xh"/><OMV name="yh"/>
    </OMBVAR>
    <OMA><OMS cd="list1" name="list"/>
         <OMA><OMS cd="arith1" name="plus"/>
              <OMV name="xA"/><OMV name="yA"/>
        </OMA>
        <OMA><OMS cd="arith1" name="plus"/>
             <OMV name="xB"/><OMV name="yB"/>
        </OMA>
        <OMA><OMS cd="fns2" name="apply_to_list"/>
             <OMA><OMS cd="arith1" name="plus"/>
                  <OMA><OMS cd="list1" name="list"/>
                       <OMA><OMS cd="arith1" name="times"/>
                            <OMV name="xa"/><OMV name="xB"/>
                       </OMA>
                       <OMA><OMS cd="arith1" name="times"/>
                            <OMV name="ya"/><OMV name="yB"/>
                       </OMA>
                       <OMV name="za"/>
                  </OMA>
             </OMA>
        </OMA>
        <OMA><OMS cd="arith1" name="plus"/>
              <OMV name="xa"/><OMV name="za"/>
        </OMA>
        <OMA><OMS cd="fns2" name="apply_to_list"/>
             <OMA><OMS cd="arith1" name="plus"/>
                  <OMA><OMS cd="list1" name="list"/>
                       <OMA><OMS cd="arith1" name="times"/>
                            <OMV name="xA"/><OMV name="xb"/>
                       </OMA>
                       <OMA><OMS cd="arith1" name="times"/>
                            <OMV name="yA"/><OMV name="yb"/>
                       </OMA>
                       <OMV name="zb"/>
                  </OMA>
             </OMA>
        </OMA>
        <OMA><OMS cd="arith1" name="plus"/>
           <OMV name="xb"/><OMV name="zb"/>
        </OMA>
        <OMA><OMS cd="fns2" name="apply_to_list"/>
             <OMA><OMS cd="arith1" name="plus"/>
                  <OMA><OMS cd="list1" name="list"/>
                       <OMA><OMS cd="arith1" name="times"/>
                            <OMA><OMS cd="arith1" name="minus"/>
                                 <OMV name="xA"/><OMV name="xB"/>
                            </OMA>
                            <OMV name="xh"/>
                       </OMA>
                       <OMA><OMS cd="arith1" name="times"/>
                            <OMA><OMS cd="arith1" name="minus"/>
                                 <OMV name="yA"/><OMV name="yB"/>
                            </OMA>
                            <OMV name="yh"/>
                       </OMA>
                       <OMI>-1</OMI>
                  </OMA>
             </OMA>
        </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

Strict Content MathML

<math xmlns="http://www.w3.org/1998/Math/MathML">
 <bind><csymbol cd="fns1">lambda</csymbol>
  <bvar><ci>xh</ci></bvar>
  <bvar><ci>yh</ci></bvar>
  <apply><csymbol cd="list1">list</csymbol>
   <apply><csymbol cd="arith1">plus</csymbol><ci>xA</ci><ci>yA</ci></apply>
   <apply><csymbol cd="arith1">plus</csymbol><ci>xB</ci><ci>yB</ci></apply>
   <apply><csymbol cd="fns2">apply_to_list</csymbol>
    <apply><csymbol cd="arith1">plus</csymbol>
     <apply><csymbol cd="list1">list</csymbol>
      <apply><csymbol cd="arith1">times</csymbol><ci>xa</ci><ci>xB</ci></apply>
      <apply><csymbol cd="arith1">times</csymbol><ci>ya</ci><ci>yB</ci></apply>
      <ci>za</ci>
     </apply>
    </apply>
   </apply>
   <apply><csymbol cd="arith1">plus</csymbol><ci>xa</ci><ci>za</ci></apply>
   <apply><csymbol cd="fns2">apply_to_list</csymbol>
    <apply><csymbol cd="arith1">plus</csymbol>
     <apply><csymbol cd="list1">list</csymbol>
      <apply><csymbol cd="arith1">times</csymbol><ci>xA</ci><ci>xb</ci></apply>
      <apply><csymbol cd="arith1">times</csymbol><ci>yA</ci><ci>yb</ci></apply>
      <ci>zb</ci>
     </apply>
    </apply>
   </apply>
   <apply><csymbol cd="arith1">plus</csymbol><ci>xb</ci><ci>zb</ci></apply>
   <apply><csymbol cd="fns2">apply_to_list</csymbol>
    <apply><csymbol cd="arith1">plus</csymbol>
     <apply><csymbol cd="list1">list</csymbol>
      <apply><csymbol cd="arith1">times</csymbol>
       <apply><csymbol cd="arith1">minus</csymbol><ci>xA</ci><ci>xB</ci></apply>
       <ci>xh</ci>
      </apply>
      <apply><csymbol cd="arith1">times</csymbol>
       <apply><csymbol cd="arith1">minus</csymbol><ci>yA</ci><ci>yB</ci></apply>
       <ci>yh</ci>
      </apply>
      <cn type="integer">-1</cn>
     </apply>
    </apply>
   </apply>
  </apply>
 </bind>
</math>

Prefix

lambda [ xh yh ] . (list (plus ( xA, yA) , plus ( xB, yB) , apply_to_list (plus (list (times ( xa, xB) , times ( ya, yB) , za) ) ) , plus ( xa, za) , apply_to_list (plus (list (times ( xA, xb) , times ( yA, yb) , zb) ) ) , plus ( xb, zb) , apply_to_list (plus (list (times (minus ( xA, xB) , xh) , times (minus ( yA, yB) , yh) , -1) ) ) ) )

Popcorn

fns1.lambda[$xh, $yh -> [$xA + $yA , $xB + $yB , fns2.apply_to_list([$xa * $xB , $ya * $yB , $za]) , $xa + $za , fns2.apply_to_list([$xA * $xb , $yA * $yb , $zb]) , $xb + $zb , fns2.apply_to_list([($xA - $xB) * $xh , ($yA - $yB) * $yh , -1])]]

Rendered Presentation MathML

$$\lambda \hspace{0.17em}\mathrm{xh},\mathrm{yh}.\begin{array}{c}\mathrm{xA}+\mathrm{yA}\hfill \\ \mathrm{xB}+\mathrm{yB}\hfill \\ \mathrm{apply\_to\_list}\left((\mathrm{xa}\mathrm{xB},\mathrm{ya}\mathrm{yB},\mathrm{za})\right)\hfill \\ \mathrm{xa}+\mathrm{za}\hfill \\ \mathrm{apply\_to\_list}\left((\mathrm{xA}\mathrm{xb},\mathrm{yA}\mathrm{yb},\mathrm{zb})\right)\hfill \\ \mathrm{xb}+\mathrm{zb}\hfill \\ \mathrm{apply\_to\_list}\left(\begin{array}{c}(\mathrm{xA}-\mathrm{xB})\mathrm{xh}\hfill \\ (\mathrm{yA}-\mathrm{yB})\mathrm{yh}\hfill \\ -1\hfill \end{array}\right)\hfill \end{array}$$

Signatures:

sts

polynomial_assertion

Description:

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

Signatures:

sts