[isabelle-dev] "canonical" left-fold combinator for lists

Makarius makarius at sketis.net
Fri Jan 13 11:13:46 CET 2012


On Fri, 13 Jan 2012, Brian Huffman wrote:

> I am writing about the following recent changeset, which adds another
> left-fold operator to HOL/List.thy.
>
> author	haftmann
> 	Fri Jan 06 10:19:49 2012 +0100 (6 days ago)
> changeset 46133	d9fe85d3d2cd
> parent 46132 	5a29dbf4c155
> child 46134 	4b9d4659228a
> incorporated canonical fold combinator on lists into body of List
>   theory; refactored passages on List.fold(l/r)
>
> http://isabelle.in.tum.de/repos/isabelle/rev/d9fe85d3d2cd
>
> I would like to take issue with a couple of things here. First, I
> don't understand why it should be called "canonical". What mainstream
> programming language has a left-fold operation with this particular
> type signature? The only place I have ever seen this variety of fold
> is in src/Pure/General/basics.ML in the Isabelle distribution.

"Canonical" is a technical term from the Isabelle/ML culture.  The idea 
behind it is already firmly established for many years, the name is there 
for quite a few years as well.  The Isabelle/Isar Implementation Manual 
privides some text on this in section 0.3.  (Does anybody have a PDF to 
Stone-Tablet-Printer?)

I've never claimed myself that the HOL library or any other language out 
there is or has to be canonical in that sense, although it would do them 
good.


 	Makarius



More information about the isabelle-dev mailing list