[Agda] RE: Z in constructive type theory

[Thomas ANBERREE]

Hi everyone,


(I'm Thomas from Nottingham Chinese Campus ).

Commenting on the two approaches to implement the ring of
integers Z from the monoid of natural numbers N:

1) Z is viewed a N+N with the injections pos, nonpos: N -> Z
mentioned by Bengt. I'm not sure this approach is less awkward
than the second mentioned. Definitions and proofs of properties
of the basic ring structure involve case analysis (between
positive and non-positive) which clutter proofs and definitions.
A stronger disadvantage could be the lack of nice
generalisations when constructing rational numbers and real
numbers.

2) Z is viewed as the quotient, NxN/~ where (m,n)~(m',n') iff
m-n=m'-n'. (This is the standard approach in classical maths
studies.)


As reminded by Nils, it might actually be easier to work at the
level of representations (pairs (m,n) in NxN) when defining and
proving properties of basic operations. One of our student (Li
Nuo) has worked on both approaches in Agda. Distributivity of
multiplication over addition was a lot shorter to prove when
working with (m,n)-representations rather than with the
quotient NxN/~ directly.

However, one's aim should be to lift results from the
representations level to a data type for integers where
definitional equality is the one between integers, such as
NxN/~ (without this, one should not call it Z). To make it
easier, one could work with normal forms (canonical
representatives) among pairs of natural numbers (e.g. n is
(0,n) and -m=(m,0)) rather than with a more abstract quotient
space. However when generalising this technique to other sets
of numbers, the use of normal forms might become more
complicated (see rational numbers) or even impossible (real
numbers).

Best, Thomas.



> From: Thorsten Altenkirch [txa at Cs.Nott.AC.UK]
> Sent: Thursday, September 24, 2009 7:59 PM
> To: Thomas ANBERREE
> Subject: Fwd: Z in constructive type theory
>
> Hi Thomas,
>
> could you add something to this. I am a bit busy in the moment.
>
> Cheers,
> Thorsten
>
> Begin forwarded message:
>
>> From: Nils Anders Danielsson <nad at cs.nott.ac.uk>
>> Date: 24 September 2009 12:49:22 BST
>> To: Bengt Nordstrom <bengt at chalmers.se>
>> Cc: Guy Wallet <guy.wallet at wanadoo.fr>,  Coquand Thierry <coquand at chalmers.se 
>> >, Thorsten Altenkirch <txa at Cs.Nott.AC.UK>
>> Subject: Re: Z in constructive type theory
>>
>> On 2009-09-21 12:49, Bengt Nordstrom wrote:
>>> The first is to use an inductive definition with two clauses, one  
>>> for positive numbers and one for non-positive numbers.
>>>  pos : Nat -> Z
>>>  nonpos : Nat -> Z
>>> The second is to use a  pair of naturals (the number being their  
>>> difference) with an explicit equality. But this is probably  
>>> awkward to work with.
>>
>> Thorsten Altenkirch has argued for using a definition with canonical
>> representatives, so that actual and propositional equality  
>> coincide, but
>> to translate to and from the representation with a pair of naturals  
>> when
>> defining functions and proofs, because that representation is  
>> easier to
>> work with.
>>
>> -- 
>> /NAD
>
> This email has been scanned by the Altman Email Security System. For  
> more information please visit www.altman.co.uk/emailsystems
> This message has been checked for viruses but the contents of an  
> attachment may still contain software viruses, which could damage  
> your computer system: you are advised to perform your own checks.  
> Email communications with the University of Nottingham may be  
> monitored as permitted by UK legislation.
> This email has been scanned by the Altman Email Security System. For  
> more information please visit www.altman.co.uk/emailsystems


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

*******************************************************************************************************************************
This email has been scanned by the Altman Email Security System.
For more information please visit www.altman.co.uk/emailsystems

*******************************************************************************************************************************
*******************************************************************************************************************************
This email has been scanned by the Altman Email Security System.
For more information please visit www.altman.co.uk/emailsystems

*******************************************************************************************************************************