*To*: bwolff at inf.ethz.ch*Subject*: Re: [isabelle] fold definitions over sets*From*: nipkow at in.tum.de*Date*: Thu, 23 Feb 2006 08:46:21 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1140604858.5659.61.camel@localhost.localdomain> (message from Burkhart Wolff on Wed, 22 Feb 2006 11:40:58 +0100)*References*: <1140604858.5659.61.camel@localhost.localdomain>

Burkhart Wolff wrote: > recently, I came across an alternative way to define > a fold on finite sets. In contrast to the Isabelle > library version (discussed in the recent TPHOLs Paper), > it has a slightly more general type: > > fold : [['a, 'b] => 'b, 'b, 'a set] => 'b The library version has type (b => b => b) => (a => b) => b => a set => b which is not more specific but simply different. The one you suggest is the one used in HOL4 which we briefly mention towards the end of section 2.2 where we also give a reference [2] that shows that both combinators are interdefinable. Ours is based on the singleton-union (SU) view of set generation, the one in HOL4 on the insert (I) view. > It is strictly more general: see above. > you can define the cardinality of finite sets by this fold, but not > by the old one, for example. At the end of section 3.5 we show how to define card in terms of our fold. The one point that does make the I-fold more attractive than the SU-fold is complexity: it is obvious how to define the latter in terms of the former, but tricky the other way around. In fact, the tricky direction leads to a situation where you call the SU-fold with a function which is not commutative in general but only on the arguments arising in that computation. Hence our library (ie the thms) would need to be generalized a little to accommodate this situation. Just like the requirement of left-commutativity for the argument of the I-fold is too strong in general. > The same algorithmic scheme would work for multi-sets too, The duality between SU and I works for sets/multisets/lists. See [2] for the details. > B) Wouldn't it be a better candidate > for the Isabelle/HOL library? If there were multiple instances where the SU-fold is more cumbersome to use than the I-fold, I might agree. But I am only aware of one instance, transitive closure, and that is defined very differently anyway. Tobias [2] @inproceedings{TannenS-ICALP91, author={Val Breazu-Tannen and Ramesh Subrahmanyam}, title = {Logical and computational aspects of programming with sets/bags/lists}, booktitle = {Automata, Languages and Programming (ICALP91)}, editor={J. Leach Albert and B. Monien and M. Rodr\'{\i}guez-Artalejo}, year = {1991}, pages = {60-75}, publisher = {Springer},series={LNCS},volume=510 }

**References**:**[isabelle] fold definitions over sets***From:*Burkhart Wolff

- Previous by Date: [isabelle] typecheck a term
- Next by Date: [isabelle] HOR 2006: call for abstracts
- Previous by Thread: [isabelle] fold definitions over sets
- Next by Thread: [isabelle] Workshop on Automated Reasoning: Call for Participation
- Cl-isabelle-users February 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list