Email Gateway (Aug 18 2022 at 15:39): Email Gateway (Aug 18 2022 at 15:39):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hello all,
since the code generator now can also handle invariants, I encapsulated
the associative lists in the Isabelle/HOL library with the distinctness
predicate as an abstract type
typedef (open) ('k, 'v) assoc_list =
"{xs :: ('k × 'v) list. distinct (map fst xs)}"
morphisms impl_of Assoc_List
by(rule exI[where x="[]"]) simp
and lifted all primitive operations and their correctness statements
from ('k * 'v) list to ('k, 'v) assoc_list. Now, I would like to go one
step further and define a trie which uses these associative lists to
manage the successor nodes:
datatype ('k, 'v) trie =
Trie "'v option" "('k, ('k, 'v) trie) assoc_list"
However, the datatype package complains that ('k, ('k, 'v) trie)
assoc_list is a non-admissible type expression which must not be used in
a nested recursion.
How can I define tries where all lists for the successor nodes are
distinct? Do I really have to go back to lists and explicit data
structure invariants and do the lifting all over again? I hope there is
a much more elegant solution to this.
Best regards,
Andreas
Email Gateway (Aug 18 2022 at 15:41):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
datatype ('k, 'v) trie =
Trie "'v option" "('k, ('k, 'v) trie) assoc_list"However, the datatype package complains that ('k, ('k, 'v) trie)
assoc_list is a non-admissible type expression which must not be used in
a nested recursion.
this restriction is not just a technical one: to be able to construct
the datatype representation, the datatype package must how to recurse
through other types involving recursion, and therefore these must
satisfay a couple of properties (which assoc_list doesn't).
How can I define tries where all lists for the successor nodes are
distinct? Do I really have to go back to lists and explicit data
structure invariants and do the lifting all over again? I hope there is
a much more elegant solution to this.
Without having an example at hand, I would deem that this is largely a
matter whether you are able to organize your proofs in a way that you
can reuse the already proven properties of assoc_list representations.
Experience however shows that fundamental constructions over datatypes
must consider the construction of the datatype anyway, so this might be
illusory.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 15:41):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Florian,
datatype ('k, 'v) trie =
Trie "'v option" "('k, ('k, 'v) trie) assoc_list"However, the datatype package complains that ('k, ('k, 'v) trie)
assoc_list is a non-admissible type expression which must not be used in
a nested recursion.this restriction is not just a technical one: to be able to construct
the datatype representation, the datatype package must how to recurse
through other types involving recursion, and therefore these must
satisfay a couple of properties (which assoc_list doesn't).
You are right, the datatype definition unfolds nested recursion into
mutual recursion. However, since assoc_list builds on the list and
product datatypes, the manual unfolding and repackaging could be
automated some time. Essentially, assoc_list is just a (degenerated)
quotient type over list with the PER xs ~ ys <--> xs = ys & distinct
(map fst ys). The quotient package already offers some support for
lifting quotients over other type constructors, but this still has to be
done manually. Are there any plans to integrate more tightly datatypes,
abstract code generator types and the quotient package?
Without having an example at hand, I would deem that this is largely a
matter whether you are able to organize your proofs in a way that you
can reuse the already proven properties of assoc_list representations.
Experience however shows that fundamental constructions over datatypes
must consider the construction of the datatype anyway, so this might be
illusory.
Since the above quotient construction can be lifted over to the trie
datatype, I think the datatype as mentions above can be constructed
manually with the free constructor Trie and an induction rule. However,
doing all this manually is probably not worth the effort.
Cheers,
Andreas
Last updated: May 06 2024 at 20:16 UTC