Email Gateway (Nov 04 2020 at 10:35): Email Gateway (Nov 04 2020 at 10:35):From: David Kretzmer <david.k@posteo.de>
Hi all,
I have defined the transitive closure of an inductive predicate as follows:
inductive less_equal_step :: "nat ⇒ nat ⇒ bool" where
"a + 1 = b ⟹ less_equal_step a b"
definition less_equal :: "nat ⇒ nat ⇒ bool" where
(* Define the transitive closure using the provided rtranclp *)
"less_equal a b ≡ (rtranclp less_equal_step) a b"
code_pred(modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) less_equal_step .
code_pred
(modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool)
[inductify]
less_equal .
(* Terminates *)
value "less_equal 1 2"
(* Does not terminate *)
value "less_equal 2 1"
Whenever less_equal does not hold execution does not terminate.
In an older email
(https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-April/msg00051.html)
I read that this is being worked on. Then in Section 2.3 of the paper
"Animating the Formalised Semanticsof a Java-like Language"
(https://pp.ipd.kit.edu/uploads/publikationen/lochbihler11itp.pdf) it
sounds like a tabled version has already been implemented. Do I have to
activate this feature somehow? Or are there other problems with the
above inductive predicate?
Best regards,
David
Email Gateway (Nov 04 2020 at 11:35):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
There is no automatic tabled execution support; that would be actually
interesting but quite tricky to get properly done in full generality.
However, I think even a tabled version would not terminate because the
table would just be filled with infinite entries following this
sequence (2, 1), (3, 1), (4, 1), (5, 1), ... and never terminate.
For this simple example, it is of course better to just use a
different but equivalent definition of less_equal_step, that
terminates under all modes.
Non-terminating rules are well known in Logic Programming; it is a
programming language paradigm that provides enough rope to hang
yourself, and it requires some knowledge of the underlying execution
principles to get a program that is reasonable executable.
I hope that helps.
Lukas
Email Gateway (Nov 04 2020 at 14:50):From: David Kretzmer <david.k@posteo.de>
Thanks, good to know! The example I gave apparently doesn't really
capture my use case, which is defining a subclass relation for a
programming language (slightly simplified version below). Since there
exists a top-most class from which all other classes derive the problem
of infinite sequences should not arise, I think.
Do you know what one has to do to get tabled execution?
type_synonym class_name = string
record class_def =
cname :: class_name
super :: "class_name option"
type_synonym program = "class_def list"
definition lookup_class :: "program ⇒ class_name ⇒ class_def option" where
"lookup_class P C ≡ find (λcl. (class_def.cname cl) = C) P"
inductive is_subclass1 :: "program ⇒ class_name ⇒ class_name ⇒ bool"
where
"⟦
Some cl = lookup_class P C;
(class_def.super cl) = Some C'
⟧ ⟹ is_subclass1 P C C'"
definition is_subclass_rtc :: "program ⇒ class_name ⇒ class_name ⇒
bool" where
"is_subclass_rtc P C C' ≡ (is_subclass1 P)⇧*⇧* C C'"
code_pred(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool) is_subclass1 .
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
[inductify]
is_subclass_rtc .
From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear David,
The tabled execution for the reflexive transitive closure is implemented in the theory
"HOL-Library.Transitive_Closure_Table", so you have to import the theory. You may also
want to have a look at the theories in JinjaThreads, where I've used tabulation for a
similar subclass relation. In particular,
https://www.isa-afp.org/browser_info/current/AFP/JinjaThreads/TypeRel.html
Section "Code Generation".
Hope this helps
Andreas
Email Gateway (Nov 04 2020 at 20:21):From: David Kretzmer <david.k@posteo.de>
Hello Andreas,
I imported "HOL-Library.Transitive_Closure_Table" and it just worked.
Thank you! I will also have a look at JinjaThreads.
Best regards,
David
Last updated: Apr 24 2024 at 08:20 UTC