Contents    Page-10    Prev    Next    Page+10    Index   

Domain Theory

A domain theory provides a logical language for the application domain:

∀ tc (= (absctt UTC tc)
         (absctt Ephemeris (UTC2Ephemeris tc)))

∀ tc (= (absctt Ephemeris tc)
         (absctt UTC (Ephemeris2UTC tc)))

absctt abstracts from a time system and time coordinate to an abstract time. These axioms specify what the conversion functions such as Ephemeris2UTC do.

Representation conversions are combinatorially explosive because they can loop.