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.


	Makarius


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