types - 如何在 Z3 中定义更高的归纳类型

Question

高级归纳类型是同伦类型理论中非常重要的工具。我正在尝试使用 Z3-SMT-LIB 定义一些更高的归纳类型。一个例子是圆，它是由一个点base和一条路径自由生成的loop，从base到它自己。我正在使用代码

(declare-datatypes () ((Circle base (loop (Circle Circle)))))
(declare-fun x1 () Circle)
(declare-fun x2 () Circle)
(assert (not (= x1 x2)))
(check-sat)
(get-model)

输出是

sat 
(model 
 (define-fun x2 () Circle (loop base)) 
 (define-fun x1 () Circle base) )

问题是：我真的在定义更高的归纳类型，叫做圆？

Answer 1

请注意，Z3 仅支持一阶归纳类型。你提供的也是一等的。