Re: [isabelle] Where to learn about HOL vs FOL?
On Mon, 4 Feb 2013, Yannick Duchêne (Hibou57) wrote:
See the Isabelle/Isar implementation manual chapter 2, about Isabelle/Pure
as reduced version of Higher-Order Logic to provide the logical framework.
This is occasionally interesting to know, although just some tiny
foundational bit. From Isabelle/Pure you move on to Isabelle/HOL,
But Isabelle/HOL is entirely derived from Isabelle/Pure, isn't it?
Isabelle/HOL is an application within Isabelle/Pure. Isabelle/Pure has
some magic bootstrapping to get the core logical framework with lots of
add-on infrastructure for Isabelle/ML in place. This magic stops just
after loading the Pure.thy and shipping the result as "Isabelle/Pure"
image. Then comes HOL and loads tons of conventional Isabelle theories
and tool implementations on top, and ships that as "Isabelle/HOL" image.
So in some sense Isabelle/HOL is indeed derived from Isabelle/Pure, for a
suitable definition of "derived".
What is also interesting that the final end-user view tends to converge
to what totally different systems offer here, e.g. Coq with its quite
different foundations, if you take inductive definitions or recursive
functions, for example.
People seems to care, only when they have to port some proof from one
system to another. There seems to be multiple HOL4 to Isabelle papers on
the web, and seems all are concerned with foundations.
These converters usually try to convert the "object-code". There are
interesting ongoing projects like
https://www.rocq.inria.fr/deducteam/Dedukti/ with potentially interesting
applications of moving huge lambda terms back and forth between systems.
The high-level problem of moving huge applications from prover X to prover
Y is not addressed at all.
This archive was generated by a fusion of
Pipermail (Mailman edition) and