Hi Manuel,

Indeed, generic iteration over a set is only well-defined if the set is finite. For an infinite set, the generic iteration combinator returns an unspecified value, not 0 or 1. In fact, I had imagined a code equation like you described, namely


  "Gcd A = (if finite A then ... else Code.abort (Gcd A))"

Note that this does *not* pull in finite_UNIV. We could implement the 
finiteness test by

  "finite (set xs) = True"
  "finite (List.coset ys) = Code.abort (STR ''Finiteness test on Complement'') 
..."

If one imports HOL/Library/Card_UNIV or Containers, then one has to provide instances for finite_UNIV and a bunch of other type classes anyways. That's the price of using more complicated libraries.

AFAICS, it does not really matter whether the iteration combinator takes an additional argument, because they can be expressed in terms of each other:

  fold_default dflt f A x = (if finite A then dflst A else Finite_Set.fold f A 
x)
  Finite_Set.fold f A x = fold_default (%A. THE ... A ...) f A x

The advantage of fold_default with a default value is that the finiteness test remains inside the implementation library B whereas with Finite_Set.fold, the finiteness test must be done whenever one wants to use the combinator. So this might be an argument in favour of fold_default.

Andreas

On 03/10/16 16:27, Manuel Eberl wrote:
I'm afraid it's not quite as easy as that. You cannot use the existing
combinators for comp_fun_commute for Gcd. For infinite sets, these
combinators return the neutral element (i.e. "0" for Gcd and "1" for
Lcm), but not every infinite set has Gcd 0 or Lcm 1. For setsum/setprod,
this works because it is quite simply defined that way, but for Gcd/Lcm
it is not.

So the alternative would be something like "Gcd A = (if finite A then
<combinator magic> else Code.abort …)". This does not work well either,
because it requires being able to decide "finite A", which typically
introduces the unwanted typeclass requirement "finite_UNIV".

My suggestion would be a combinator that, in order to implement a
function f :: 'a set => 'a, takes as arguments both a fold operation of
type "'a cfc" /and/ the function f itself.

It then performs the fold on any "finite by construction" set (e.g. sets
represented by the "set" constructor) and returns "Code.abort … (f A)"
for anything else (e.g. a set represented by the "coset" constructor).

I planned on implementing this at some point, but I've quite a bit of
other stuff to do and I wanted to discuss it first, so I never really
got around to doing it.

Cheers,

Manuel


On 03/10/16 16:15, Andreas Lochbihler wrote:
Hi René and Manuel,

Indeed, for sets, expressing the code equations in terms of a generic
iteration operation on sets would do the job for most of the cases. The
comp_fun_commute and comp_fun_idem types  in Containers precisely do
this, but they have not been integrated in the HOL library yet. They
should work all kinds of big operators (setsum, setprod, Gcd, etc) and
could be added to the HOL library.

Of course, some special case tricks no longer work if go for a generic
iteration operation. For example, one could prove "Gcd (List.coset xs) =
1" for natural numbers and declare a code equation. Such things would no
longer be possible, but I am not sure whether they are done at all at
the moment.

Manuel's suggestion of code_abort is a bit cleaner than René's use
Code.abort, because Code.abort does not work with normalisation by
evaluation whereas code_abort does.

Best,
Andreas


On 03/10/16 15:29, Manuel Eberl wrote:
This is a problem that I have given quite some thought in the past. The
problem is the following: You have a theory A providing certain
operations on sets (in this case: Gcd) and a theory B providing
implementations for sets (in this case: Containers).

The problem is that the code equations for the operations from A depend
on the implementation that is chosen for sets. A cannot give code
equations for every possible implementation of sets, while B cannot
possibly import every theory that has operations involving sets and give
code equations for it.

The best possible solution would be to imitate the way it is currently
done for setsum, setprod, etc: Define a sufficiently general combinator
that iterates over the set and give the code equations in A in terms of
this combinator. Then B only has to reimplement this generic combinator.

That would be the cleanest solution, but I'm not sure how such a
combinator would look like. The folding operation would probably have to
satisfy some associativity/commutativity laws and have that information
available at the type level (similar to the cfc type in Containers).


By the way, my current workaround for this problem is to declare all
problematic constants as "code_abort".


Cheers,

Manuel


On 03/10/16 15:21, Thiemann, Rene wrote:
Dear all,

in the following theory, the export-code fails:

(Isabelle 957ba35d1338, AFP 618f04bf906f)

theory Problem
  imports
  "~~/src/HOL/Library/Polynomial_Factorial"
  "$AFP/thys/Containers/Set_Impl"
begin

definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where
  "foo x y = gcd y x"

definition bar :: "int ⇒ int" where
  "bar x = foo x (x - 1)"

export_code bar in Haskell
end


The problem arises from two issues:
- factorial_semiring_gcd requires code for
  Gcd :: “Set ‘a => ‘a”, not only for the binary “gcd :: ‘a => ‘a =>
‘a”!
- the code-equation for Gcd is Gcd_eucl_set: "Gcd_eucl (set xs) =
foldl gcd_eucl 0 xs”
  where “set” is only a constructor if one does not load the
container-library.

It would be nice, if one can either alter factorial_semiring_gcd so
that it does not
require “Gcd” anymore, or if the code-equation is modified in a way
that permits
co-existence with containers. (Of course, similarly for Lcm).


With best regards,
Akihisa, Sebastiaan, and René

PS: We currently solve the problem by disabling Gcd and Lcm as follows:

lemma [code]: "(Gcd_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Gcd
on sets'') (λ _. Gcd_eucl)"  by simp
lemma [code]: "(Lcm_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Lcm
on sets'') (λ _. Lcm_eucl)"  by simp
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to