Email Gateway (Aug 18 2022 at 16:57): Email Gateway (Aug 18 2022 at 16:57):From: Steve W <s.wong.731@gmail.com>
Hi,
I have a question about Isabelle's polymorphism. Since Isabelle has a
simply-typed lambda calculus, how come the meta-logic is polymorphic?
Polymorphism is not typically considered simple, right?
Regards
Steve
Email Gateway (Aug 18 2022 at 16:58):From: Makarius <makarius@sketis.net>
Funny thing (1): Isabelle/Pure is not really a meta-logic, because it
cannot reason much about other logics. This is why I prefer to call it
"logical framework", according to what I've learned from Stefan Berghofer
at some point.
Funny thing (2): Isabelle/Pure is not polymorphic either. You can work
schematically wrt. arbitrary types and the system juggles contexts and
results in a way that it looks like Hindley-Milner polymorphism. See also
the explanation of the "admissible rules generalize and instantiate" in
the Isabelle/Isar implementation manual (chapter 2).
Makarius
Email Gateway (Aug 18 2022 at 16:58):From: Makarius <makarius@sketis.net>
Moreover see the following paper on local theory specifications:
Florian Haftmann and Makarius Wenzel. Local theory specifications in
Isabelle/Isar, In S. Berardi, F. Damiani and U. de Liguoro, editors,
Types for Proofs and Programs, TYPES 2008. LNCS 5497, Springer, 2009.
http://www4.in.tum.de/~wenzelm/papers/local-theory.pdf
At the end of section 3 it says:
Here the type variables 'a need to be fixed in the context, but ?'b is
arbitrary. In other words, we have conjured up proper let-polymorphism
in the abstract syntax layer of Isabelle/Isar, without touching the Pure
logic. [By extending it towards a more complicated system with
polymorphism.]
See also the example
http://isabelle.in.tum.de/dist/library/HOL/ex/Abstract_NAT.html which
defines a "polymorphic" recursion operator on a hypothetical type of
natural numbers.
Makarius
Email Gateway (Aug 18 2022 at 16:58):From: Tobias Nipkow <nipkow@in.tum.de>
Isabelle's lambda calculus is in between simply typed and ML-style
polymorphic (with type classes thrown in). It is simply typed because
the types are built up from base types by means of =>. It resembles
ML-style polymorphism because it has type variables, too (and thus
simply-typed is an understatement). The difference to ML-style
polymorphism is that it has no let construct for defining a polymorphic
constant locally inside a term. This has to be done at the declaration
level, i.e. gobally. It shares the absence of explicit type quantifiers
with Milner's original paper, where he even managed to have a
let-construct without making the quantifiers explicit.
Tobias
Steve W schrieb:
Email Gateway (Aug 18 2022 at 16:58):From: mark@proof-technologies.com
Actually the term "simply-typed" tends to be used in more than one way.
Some people use it to mean "not dependently-typed" and some people use it to
mean "not polymorphic and not dependently-typed".
When people refer to "simply-typed lambda calculus" they are (usually)
referring to Church's original simply typed lambda calculus (which he
created after his untyped lambda calculus). This does not have
polymorphism, but Isabelle and HOL, that are based on it, do.
Mark.
on 17/1/11 6:01 PM, Steve W <s.wong.731@gmail.com> wrote:
Last updated: Apr 25 2024 at 12:23 UTC