OpenMath Content Dictionary: rounding1

Canonical URL:
http://www.openmath.org/cd/rounding1.ocd
CD File:
rounding1.ocd
CD as XML Encoded OpenMath:
rounding1.omcd
Defines:
ceiling, floor, round, trunc
Date:
2001-03-12
Version:
2
Review Date:
2003-04-01
Status:
official
Uses CD:
quant1, logic1, relation1, arith1, alg1, set1, setname1

A CD of basic rounding concepts

Written by James Davenport, inspired by the need from bigfloat.ocd.
Finished 1999-10-24.

ceiling

The round up (to +infinity) operation.

Commented Mathematical property (CMP):
for all x | ceiling(x)-1 < x <= ceiling x
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="relation1" name="lt"/>
        <OMA>
          <OMS cd="arith1" name="minus"/>
          <OMA>
            <OMS cd="rounding1" name="ceiling"/>
            <OMV name="x"/>
          </OMA>
          <OMS cd="alg1" name="one"/>
        </OMA>
        <OMV name="x"/>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="leq"/>
        <OMV name="x"/>
        <OMA>
          <OMS cd="rounding1" name="ceiling"/>
          <OMV name="x"/>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (and (lt (minus (ceiling ( x) , one) , x) , leq ( x, ceiling ( x) ) ) )

Signatures:
sts


[Next: floor] [Last: round] [Top]

floor

The round down (to -infinity) operation.

Commented Mathematical property (CMP):
for all x | floor(x) <= x < floor(x)+1
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="relation1" name="lt"/>
        <OMV name="x"/>
        <OMA>
          <OMS cd="arith1" name="plus"/>
          <OMA>
            <OMS cd="rounding1" name="floor"/>
            <OMV name="x"/>
          </OMA>
          <OMS cd="alg1" name="one"/>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="leq"/>
        <OMA>
          <OMS cd="rounding1" name="floor"/>
          <OMV name="x"/>
        </OMA>
        <OMV name="x"/>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (and (lt ( x, plus (floor ( x) , one) ) , leq (floor ( x) , x) ) )

Signatures:
sts


[Next: trunc] [Previous: ceiling] [Top]

trunc

The round to zero operation.

Commented Mathematical property (CMP):
for all x | trunc(x) <= x < trunc(x)+1 (x>0)
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="relation1" name="geq"/>
        <OMV name="x"/>
        <OMS cd="alg1" name="zero"/>
      </OMA>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="relation1" name="lt"/>
          <OMV name="x"/>
          <OMA>
            <OMS cd="arith1" name="plus"/>
            <OMA>
              <OMS cd="rounding1" name="trunc"/>
              <OMV name="x"/>
            </OMA>
            <OMS cd="alg1" name="one"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="leq"/>
          <OMA>
            <OMS cd="rounding1" name="trunc"/>
            <OMV name="x"/>
          </OMA>
          <OMV name="x"/>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (implies (geq ( x, zero) , and (lt ( x, plus (trunc ( x) , one) ) , leq (trunc ( x) , x) ) ) )

Commented Mathematical property (CMP):
for all x | trunc(x) >= x > trunc(x)-1 (x<0)
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="x"/>
    </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMS cd="relation1" name="leq"/>
          <OMV name="x"/>
          <OMS cd="alg1" name="zero"/>
        </OMA>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="relation1" name="gt"/>
            <OMV name="x"/>
            <OMA>
              <OMS cd="arith1" name="minus"/>
              <OMA>
                <OMS cd="rounding1" name="trunc"/>
                <OMV name="x"/>
              </OMA>
              <OMS cd="alg1" name="one"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="relation1" name="geq"/>
            <OMA>
              <OMS cd="rounding1" name="trunc"/>
              <OMV name="x"/>
            </OMA>
            <OMV name="x"/>
          </OMA>
        </OMA>
      </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (implies (leq ( x, zero) , and (gt ( x, minus (trunc ( x) , one) ) , geq (trunc ( x) , x) ) ) )

Signatures:
sts


[Next: round] [Previous: floor] [Top]

round

The round to nearest operation.

Commented Mathematical property (CMP):
for all x | x <= round(x)+1/2 and x <= round(x)-1/2
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="and"/>
      <OMA>
        <OMS cd="relation1" name="leq"/>
        <OMV name="x"/>
        <OMA>
          <OMS cd="arith1" name="plus"/>
          <OMA>
            <OMS cd="rounding1" name="round"/>
            <OMV name="x"/>
          </OMA>
          <OMA>
            <OMS cd="arith1" name="divide"/>
            <OMS cd="alg1" name="one"/>
	    <OMI> 2 </OMI>
          </OMA>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="relation1" name="geq"/>
        <OMV name="x"/>
        <OMA>
          <OMS cd="arith1" name="minus"/>
          <OMA>
            <OMS cd="rounding1" name="round"/>
            <OMV name="x"/>
          </OMA>
          <OMA>
            <OMS cd="arith1" name="divide"/>
            <OMS cd="alg1" name="one"/>
	    <OMI> 2 </OMI>
          </OMA>
        </OMA>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (and (leq ( x, plus (round ( x) , divide (one, 2 ) ) ) , geq ( x, minus (round ( x) , divide (one, 2 ) ) ) ) )

Commented Mathematical property (CMP):
for all x | Also round to even in event of a tie
Formal Mathematical property (FMP):
<OMOBJ>
  <OMBIND>
    <OMS cd="quant1" name="forall"/>
    <OMBVAR>
       <OMV name="x"/>
    </OMBVAR>
    <OMA>
      <OMS cd="logic1" name="implies"/>
      <OMA>
        <OMS cd="logic1" name="and"/>
	<OMA>
	  <OMS cd="logic1" name="not"/>
	  <OMA>
	    <OMS cd="set1" name="in"/>
	    <OMV name="x"/>
	    <OMS cd="setname1" name="Z"/>
	  </OMA>
	</OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMA>
	    <OMS cd="arith1" name="times"/>
  	    <OMV name="x"/>
	    <OMI> 2 </OMI>
  	  </OMA>
	  <OMS cd="setname1" name="Z"/>
        </OMA>
      </OMA>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMA>
          <OMS cd="arith1" name="divide"/>
          <OMA>
            <OMS cd="rounding1" name="round"/>
            <OMV name="x"/>
          </OMA>
	  <OMI> 2 </OMI>
        </OMA>
        <OMS cd="setname1" name="Z"/>
      </OMA>
    </OMA>
  </OMBIND>
</OMOBJ>

forall [ x ] . (implies (and (not (in ( x, Z) ) , in (times ( x, 2 ) , Z) ) , in (divide (round ( x) , 2 ) , Z) ) )

Signatures:
sts


[First: ceiling] [Previous: trunc] [Top]