Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu



On 22.08.2016 19:39, Ken Kubota wrote:
In Q0/R0 there are no such declarations.
In summary, the solution would be not allowing declarations in the mathematical language, but only definitions, like in Q0/R0.

Also, implementing definitions within the logical core contradicts to the LCF philosophy of a small trusted kernel.
For this reason, definitions in R0 are mere abbreviations located outside of the logical kernel.
They also can be removed at any time (and re-introduced again) without modifying the theorems already obtained.
Yes, such extreme measures would greatly simplify the story from a theoretical point of view, but we are talking here of implemented logic: it needs to provide extra provisions to make it usable in practice.

Abbreviations that are always expanded would render the system impractical due to huge terms in expanded internal form.

Ruling out declarations that are separated from definitions greatly simplify things, but prevent important applications like type class instantiation.


There is always a tradeoff in theoretical simplicity versus complexity required for practical applications of logic. Without that tradeoff, making a usable theorem proving environment like Isabelle would be a trivial exercise, and not an effort of 30 years.


        Makarius




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