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:
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.
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and