如何让基于record与set定义的可归纳谓词可求值？

问题描述 #

尝试为图计算定义归纳谓词min_sum，编写了如下Isabelle/HOL代码，但使用values查询{ x. min_sum G1 x }未得到预期结果{5}。需解决：

• 能否让该谓词可求值？
• 是否需要将set替换为fset、函数替换为有限映射，或是将record替换为归纳数据类型？
• 有没有其他解决方案？

type_synonym node = nat
type_synonym edge = nat

record graph =
  nodes :: "node set"
  edges :: "edge set"
  source :: "edge ⇒ node"
  target :: "edge ⇒ node"
  weight :: "edge ⇒ nat"

inductive min_sum where
  "edges G = {e} ⟹
   weight G e = x ⟹
   min_sum G x"

code_pred [show_modes] min_sum .

definition "G1 ≡ ⦇
  nodes = {1,2},
  edges = {1},
  source = (λx. undefined)(1 := 1),
  target = (λx. undefined)(1 := 2),
  weight = (λx. undefined)(1 := 5)
⦈"

(* Expected result: {5} *)
values "{x. min_sum G1 x}"

解决方案 #

核心问题分析

当前代码无法求值的关键原因：

• 标准set是无限域上的抽象集合，Isabelle代码生成器无法直接处理其相等性判断（edges G = {e}）。
• source/target/weight使用含undefined的λ表达式，代码生成器无法处理未定义的函数分支。

可行方案

方案一：改用有限集合fset与有限映射fmap

将图定义中的set替换为fset（有限集合），函数替换为fmap（有限映射），确保所有结构可枚举：

type_synonym node = nat
type_synonym edge = nat

record graph =
  nodes :: "node fset"
  edges :: "edge fset"
  source :: "edge fmap node"
  target :: "edge fmap node"
  weight :: "edge fmap nat"

inductive min_sum where
  "edges G = {|e|} ⟹
   fmap_of (weight G) e = Some x ⟹
   min_sum G x"

code_pred [show_modes] min_sum .

definition "G1 ≡ ⦇
  nodes = {|1,2|},
  edges = {|1|},
  source = fmap_of_list [(1, 1)],
  target = fmap_of_list [(1, 2)],
  weight = fmap_of_list [(1, 5)]
⦈"

values "{x. min_sum G1 x}"  (* 输出: {5} *)

方案二：保留record，用完全有限函数替代含undefined的λ表达式

若不想改用fset，可将函数定义为完全有限函数，避免undefined，同时为有限集合添加可判定性支持：

type_synonym node = nat
type_synonym edge = nat

record graph =
  nodes :: "node set"
  edges :: "edge set"
  source :: "edge ⇒ node"
  target :: "edge ⇒ node"
  weight :: "edge ⇒ nat"

(* 为有限集合相等性添加可判定性实例 *)
instance set :: (finite) finite ..

inductive min_sum where
  "edges G = {e} ⟹
   weight G e = x ⟹
   min_sum G x"

code_pred [show_modes] min_sum .

(* 用完全函数替代含undefined的定义，非edge分支设为任意确定值 *)
definition "G1 ≡ ⦇
  nodes = {1,2},
  edges = {1},
  source = (λx. if x=1 then 1 else 0),
  target = (λx. if x=1 then 2 else 0),
  weight = (λx. if x=1 then 5 else 0)
⦈"

values "{x. min_sum G1 x}"  (* 输出: {5} *)

方案三：将图定义为归纳数据类型

若图结构固定简单，可直接用归纳类型定义图，避免集合和函数的抽象性：

type_synonym node = nat
type_synonym edge = nat
type_synonym weight = nat

datatype graph = Graph "node set" "(edge × node × node × weight) list"

inductive min_sum where
  "Graph ns [(e, s, t, w)] = G ⟹ min_sum G w"

code_pred [show_modes] min_sum .

definition "G1 ≡ Graph {1,2} [(1, 1, 2, 5)]"

values "{x. min_sum G1 x}"  (* 输出: {5} *)

关键注意事项

• 可判定性：代码生成器要求谓词中的所有操作可判定，因此集合必须有限可枚举，函数必须完全定义。
• code_pred配置：确保code_pred正确生成代码，必要时可添加code_pred [code] min_sum强制生成执行代码。

内容的提问来源于stack exchange，提问作者Denis