by Thorsten on June 26, 2009.
Tagged as: Lunches.
I was talking about Li Nuo’s (our summer intern) project today. The goal is to develop a library for numbers in Agda which initially covers the integers and the rational numbers and in the long run also the Reals and the complex numbers. The goal is to establish basic algebraic properties such as that the integers are a ring and the rational numbers a field.
Instead of defining the operations on a canonical representation of numbers I suggest to define them first on a setoid and then define a normalisation operation from the setoid to the canonical representation. The laws of normalisation are the usual ones we know from the lambda calculus (e.g. look up James and my paper on big step normalisation). As I only realized after the talk it is not actually necessary to define the operation on the canonical representation – they can be simply lifted from the operation on setoids.
As we know this deosn’t work for the Reals because there is no canonical representation. A simple way to see this is to notice that all sets definable in ordinary Type Theory (w.o. quotients) have the property that if two elements are observationally equal then they are equal, where by observationally equal we mean that all functions into the booleans agree. However, this is not the case for the reals because the only functions from Real to Bool are the constant functions.
Here is the whiteboard from the talk:
numbers