Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy



On 5/22/2013 1:58 AM, Johannes Hölzl wrote:
It'd be interesting to know if it's common these days for other
languages to use the classic definition of the integers as equivalence
classes like you did with Int.thy:

https://en.wikipedia.org/wiki/Integer#Construction

It seems it's common for the natural numbers to be built using the
successor function, but I'm guessing it's not so common for the integers
to be equivalence classes.
In my experience it is quite the other way round. The first semesters
mathematics course I attended introduced the integers, the rational
numbers and the real numbers as equivalence classes. Only the natural
numbers and the complex numbers where introduced like a datatype.

Johannes,

Thanks for your comment. I was comparing the formal, textbook construction of the integers, as in what you're listing, to concrete implementations of integers in programming languages, such as Coq, Isabelle/HOL, Haskell, or any other language, old or new, but especially new.

I'm speculating that this ability of Isabelle/HOL to define integers as equivalence classes is special, and that it takes a special foundation in a language to be able to do it, and that most languages don't have the foundation to be able to do it in a practical way.

But I wouldn't know. This is the first time I've ever delved into the low-level internals of a programming language, but defining an integer as a set, in particular as an equivalence class, seems like it requires some clever and sophisticated foundational code.

First, a person would simply know how it could be done at all. But that's not enough; their code would have to perform reasonably fast.

I wouldn't know where to begin, and I'm sure any initial discovery of mine on how to do it would be so slow, it would be useless.

All that to say, I'm guessing that Isabelle/HOL is pretty special in this ability to achieve a textbook definition of the integers. But I try not to become dogmatic about things I don't know about, and it could be that it's very common for programming languages to implement integers as equivalence classes.

Regards,
GB





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.