Email Gateway (Aug 19 2022 at 17:24): Email Gateway (Aug 19 2022 at 17:24):From: Andrew Gacek <andrew.gacek@gmail.com>
I'm trying to write a function in Isabelle/HOL to generate a fresh
variable name (given a finite set of used names). I'm having trouble,
in part, because proving termination for the function requires knowing
that the set is finite (I don't care about the function output when
infinite). Does anybody have a suggestion about how to proceed?
I was hoping to create a function like
fresh_string :: string set => string => string
That might work like
fresh_string {''A'', ''B'', ''A0'', ''A1''} ''A'' = ''A2''
That is, the second argument is used as a base for the generated
variable name. And the theorem I'd want to prove is
finite xs ==> fresh_string xs y \notin xs
This is the closest I've come, but I'm not hopeful about being able to
prove termination:
fun string_of_nat :: "nat ⇒ string"
where
"string_of_nat n = (if n < 10 then [char_of_nat (48 + n)] else
string_of_nat (n div 10) @ [char_of_nat (48 + (n mod 10))])"
fun fresh_string_aux :: "string set ⇒ string ⇒ nat ⇒ string" where
"fresh_string_aux xs y n = (if finite xs then
(if y @ string_of_nat n ∈ xs then
fresh_string_aux xs y (Suc n)
else
y @ string_of_nat n)
else
undefined)"
fun fresh_string :: "string set ⇒ string ⇒ string" where
"fresh_string xs y = fresh_string_aux xs y 0"
The reason for all this is that I'm writing a function that will
require fresh variable names and I'd like to be able to actually
execute that function and get readable results.
Thanks,
Andrew
Email Gateway (Aug 19 2022 at 17:25):From: Peter Lammich <lammich@in.tum.de>
Hi,
find attached what we use in CoCon
(http://www21.in.tum.de/~popescua/rs3/CoCon.html) to generate fresh IDs.
The function "fresh" there exactly matches your signature, and
is executable.
The formalization of "fresh" is mostly by Andrei Popescu.
Fresh.thy
Email Gateway (Aug 19 2022 at 17:26):From: Tobias Nipkow <nipkow@in.tum.de>
My recommendation in such situations is to use a list rather than a set. Of
course the callers of fresh_string will also need to use lists, and so on. But
since function "set" converts a list into a set, the change is usually not very
painful.
Tobias
smime.p7s
Email Gateway (Aug 19 2022 at 17:27):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Andrew,
you can find a theory "Name" in the IsaFoR-repository.
It contains fresh-name generators for strings like the ones you desire.
(fresh_string, fresh_string_list, ...)
Hope this helps,
René
PS: IsaFoR/CeTA is freely available under http://cl-informatik.uibk.ac.at/software/ceta/
Email Gateway (Aug 19 2022 at 17:29):From: Peter Lammich <lammich@in.tum.de>
The function "fresh" there exactly matches your signature
Oops, function fresh there actually uses a list, rather than a set:
fresh :: string list => string => string
Last updated: Nov 21 2024 at 12:39 UTC