如何解决函数声明是 Constant 类型的术语,以及如何将此类函数声明转换为 Const 类?
我正在尝试使用 https://github.com/dominique-unruh/scala-isabelle 来解析和分解 Isabelle 术语,并且我试图从快速排序 https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html 的形式化中分解术语 - 函数声明 - 这个 Isabelle 代码:
function quicksort :: "'a::{heap,linorder} array ⇒ nat ⇒ nat ⇒ unit Heap"
where
"quicksort arr left right =
(if (right > left) then
do {
pivotNewIndex ← partition arr left right;
pivotNewIndex ← assert (λx. left ≤ x ∧ x ≤ right) pivotNewIndex;
quicksort arr left (pivotNewIndex - 1);
quicksort arr (pivotNewIndex + 1) right
}
else return ())"
by pat_completeness auto
我正在尝试在 Scala/Isabelle 中使用:
println("Before qs term")
val qs_term = Term(ctxt,"quicksort arr left right =" +
" (if (right > left) then" +
" do {" +
" pivotNewIndex ← partition arr left right;" +
" pivotNewIndex ← assert (λx. left ≤ x ∧ x ≤ right) pivotNewIndex;" +
" quicksort arr left (pivotNewIndex - 1);" +
" quicksort arr (pivotNewIndex + 1) right" +
" }" +
" else return ())")
println("After qs term")
我正在检查 Term 类的文档:https://javadoc.io/doc/de.unruh/scala-isabelle_2.13/latest/de/unruh/isabelle/pure/Term.html,我看到这个 Const
有 Term
构造函数:
sealed abstract class Term
final case class Const(name: String,typ: Typ) // Corresponds to ML constructor 'Const'
...
我的问题是:Isabelle 函数声明是具有类构造函数 Const
的 Term 实例吗? 我如何将我的 qs_term
转换为类 {{ 1}} 的目的是访问特定于 Const
的字段? 我的目标是对类(以 Const 类为根对象)进行树搜索(DFS、BFS)并在为这个函数声明构造 AST 的这种方式。
解决方法
您构建的不是 quicksort
的定义(至少不是在 Isabelle 中定义任何东西的意义上),而只是一个表达您想要的属性的术语强>quicksort
应该满足。
Isar 中的 function
命令(以及 definition
命令)采用规范(例如,您编写的术语)并将其内部转换为两部分:您定义的常量的名称(此处 TheoryName.quicksort
),以及一个说明 quicksort
应定义为什么的术语(此处为 λarr left right. (if ...)
)。
如果您想在 Isabelle 中以编程方式创建定义(无论是 Isabelle/ML),您需要:
- 获取上下文(例如,
Context("TheoryName")
)(或理论)。 - 应用合适的命令来创建定义。 scala-isabelle 中没有预定义的命令,因此您必须使用执行此操作的 ML 代码并使用
MLValue.compileFunction
(ScalaDoc) 对其进行包装。然后,此函数采用您的上下文(或理论)以及常量名称和术语以及更多信息,并返回具有定义值的新理论或上下文。 (例如,Local_Defs.define
中的local_defs.ML
就是这样一个函数,我认为。)
Const
类与您要问的内容无关。 Isabelle 中的一个术语是具有不同种类叶子的树。一些叶子是变量,一些叶子是常数。例如,如果您遍历快速排序项,您会发现,例如,partition
和 assert
是常量,因此使用类 Const
表示。
这是正在进行的回答。我想出了代码:
println("Before test term");
val test_term = Term(ctxt,"two_integer_max_case_def a b = (case a > b of True \\<Rightarrow> a | False \\<Rightarrow> b)")
println("After test term")
println(test_term.getClass())
println("test_term: " + test_term.pretty(ctxt))
val jsonString = write(test_term)
println("After write test term")
def t_report(term: Term,curr_string: String): String = term match {
case Const(p_name,p_type) => curr_string + " Const " + p_name
case Free(p_name,p_type) => curr_string + " Free " + p_name
case Var(p_name,p_index,p_type) => curr_string + " Var " + p_name + p_index
case Abs(p_name,p_type,p_body_term) => curr_string + " Abs " + p_name + p_body_term.pretty(ctxt) + t_report(p_body_term,curr_string)
case Bound(p_index) => curr_string + " Bound " + p_index
case App(p_term_1,p_term_2) => curr_string + " App " + p_term_1.pretty(ctxt) + t_report(p_term_1,curr_string) + p_term_2.pretty(ctxt) + t_report(p_term_2,curr_string)
//final case class Const(name: String,typ: Typ) // Corresponds to ML constructor 'Const'
//final case class Free(name: String,typ: Typ) // Corresponds to ML constructor 'Free'
//final case class Var(name: String,index: Int,typ: Typ) // Corresponds to ML constructor 'Var'
//final case class Abs(name: String,typ: Typ,body: Term) // Corresponds to ML constructor 'Abs'
//final case class Bound private (index: Int) // Corresponds to ML constructor 'Bound'
//final case class App private (fun: Term,arg: Term) // Corresponds to ML constructor '$'
case _ => curr_string + " Other "
}
println(t_report(test_term,"zero"))
此代码报告:
zero App (=) (two_integer_max_case_def a b)zero App (=)zero Const HOL.eqtwo_integer_max_case_def a bzero App two_integer_max_case_def azero App two_integer_max_case_defzero Free two_integer_max_case_defazero Free abzero Free bcase b < a of True ⇒ a | False ⇒ bzero App case_bool a bzero App case_bool azero App case_boolzero Const Product_Type.bool.case_boolazero Free abzero Free bb < azero App (<) bzero App (<)zero Const Orderings.ord_class.lessbzero Free bazero Free a
所以 - 从这个输出可以推断:
- 函数声明是 App 类型的 Term。显然,
=
是一些元级应用程序,可促进从函数体到参数的映射。 - 无需进行 Scala 或 Java 反射,所有类型都可以由 Scala
match
工具确定。
实际上 - 最重要的一点 - 我可以从这个 t_report 代码中构造 XML 或 JSON 中的抽象语法树,我只需要弄清楚这个代码构造的树访问顺序。我之前问过如何从 Isabelle 表达式构造 AST,大家都说这几乎是不可能的,但在这里它几乎是可见的?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。