归纳谓词、传递闭包和代码生成

Question

我正在将 subclass 和子类型关系定义为 Java 类语言的归纳谓词，并希望为这些关系生成代码。为子类型关系定义和生成代码没有问题：

type_synonym class_name = string

record class_def =
  cname :: class_name
  super :: "class_name option"
  interfaces :: "class_name list"

type_synonym program = "class_def list"

(* Look up a class by its name *)
definition lookup_class :: "program ⇒ class_name ⇒ class_def option" where
  "lookup_class P C ≡ find (λcl. (class_def.cname cl) = C) P"

(* Direct subclass relation *)
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'"

(* Reflexive transitive closure of `is_subclass1` *)
definition is_subclass :: "program ⇒ class_name ⇒ class_name ⇒ bool" where
  "is_subclass 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 .

这里，如果C'是C的直接superclass的名称，则is_subclass1 P C C'为真。那么is_subclass被定义为is_subclass1.

的传递闭包

要使代码生成工作，is_subclass1 具有模式 i ⇒ i ⇒ o ⇒ bool 至关重要，否则无法计算传递闭包。在 is_subclass1 的情况下，这很容易，因为 class 最多有一个直接的超级 class，因此超级 class 的名称可以唯一地确定输入。

但是，对于子类型关系，我还需要考虑 class 可能实现的接口：

inductive is_subtype1 :: "program ⇒ class_name ⇒ class_name ⇒ bool" for P :: program where
  ― ‹Same as subclass relation, no problem›
  "⟦
    Ok cl = lookup_class P C;
    Some C' = (class_def.super cl)
  ⟧ ⟹ is_subtype1 P C C'" |

  "⟦
    Ok cl = lookup_class P C;
    ― ‹HERE IS THE PROBLEM: C' cannot be uniquely derived from the inputs and can thus not be marked as an output›
    C' ∈ set (class_def.interfaces cl)
  ⟧ ⟹ is_subtype1 P C C'"

问题是 C' 有多个可能的值，它不能被标记为输出。

直觉上，我认为这对代码生成器来说应该不是问题，因为生成的代码可以迭代 class 的所有接口。但是，我不知道这是否可以用 Isabelle/HOL.

来表示

因此，问题是：有没有一种方法可以使用模式 i ⇒ i ⇒ o ⇒ bool 为 is_subtype1 生成代码？

Answer 1

您可以通过导入 HOL-Library.Predicate_Compile_Alternative_Defs 然后使用 List.member _ _ 而不是 _ ∈ set _ 来解决您的问题。

归纳谓词、传递闭包和代码生成

Inductive predicates, transitive closure, and code generation

isabelle