Lisp-PDDL 与 INVAL 规划验证器¶
Scheme 语言与 PDDL 的渊源¶
Scheme 程序设计语言的设计灵感源自麻省理工学院 Carl Hewitt 所提出的"演员模型"（Actor Model）这一数学模型。Hewitt 当时正致力于将演员模型引入 Planner 语言，受此启发的 Steele 与 Sussman 决定在 Maclisp 中实现一种支持演员模型的 Lisp 方言 [5]。Steele 与 Sussman 很快发现，演员模型与 λ 演算（Lambda Calculus）具有高度的结构相似性，而所谓"演员"实质上不过是 Peter J. Landin 提出、并由 Joel Moses 于 1970 年正式发表的闭包（Closure）概念 [6]。这一重要发现使两人深刻认识到，这正是将词法变量作用域（Lexical Scoping）引入 Lisp 实现的关键突破口 [7]。基于这一理论认识，他们迅速开发出一套极其简洁的编程语言，最初命名为"Schemer"（后因操作系统文件名长度限制而简化为 Scheme）。尽管 Hewitt 认为 Scheme 在抽象能力方面存在不足并视之为一种倒退，但其简洁优雅的语法体系迅速获得了学术界的广泛认可，并最终成为计算机科学领域最具影响力的编程语言之一。在 Scheme 被广泛接受之后，Steele 与 Sussman 曾坦言，他们实际上并未刻意追求 Scheme 的简约性。两位研究者认为，正是 λ 演算本身所固有的简洁而强大的数学特性，才使得 Scheme 得以实现极致的语言精简化 [5]。
更多关于 Scheme 语言的介绍可参考 维基百科页面。
INVAL 规划验证器¶
INVAL 是一个独立于现有实现的 PDDL 规划验证器。
背景与动机¶
规划领域定义语言（PDDL）作为一种用于表达 AI 规划问题的形式化建模语言，被广泛用作众多通用 AI 规划系统的标准输入语言。规划验证器的核心作用在于，依据给定的领域定义与问题规范，严格检验（由 AI 规划器自动生成或人工手动编写的）规划方案的有效性与正确性。验证器是对领域/问题规范、规划器实现以及 PDDL 语言规范本身进行系统性调试的极为有效的工具。
由 Derek Long 等人开发的主流 PDDL 规划验证器 VAL 功能相对完善，但与所有软件系统一样，不可避免地存在潜在缺陷。INVAL 的设计目标在于补充 VAL，而非取而代之。INVAL 旨在提供一种对学术文献中所定义 PDDL 形式语义的简洁而精确的实现（其设计理念侧重于语义忠实性，而非追求功能完备性或运行高效性）。当两个验证器对同一规划方案给出一致判定结论时，研究者可对结果的正确性具备更强的置信度；反之，若结论存在分歧，则难以确证任一结果的正确性。当两者结论相左时，则表明其中之一可能存在实现缺陷，抑或 PDDL 语言规范本身在某些语义点上存在歧义。
功能限制¶
与 VAL 相比，INVAL 存在若干功能限制。
配套工具集¶
该软件包还包含一组其他 PDDL 工具：
rsk：一个领域/问题编译器，可用于消除对象流利（Object Fluents，PDDL 3.1 版本特性）。它既能够完全编译去除对象流利（生成类似于 ADL 的标准 PDDL），也可以仅编译嵌套的流利表达（生成类似于 SAS+ 的形式化表达）。simplify：领域/问题简化程序。其输出为"简单 ADL"（Simple ADL），该表达形式可能仍然包含条件作用，但不含量词或析取项。nyat：可将 PDDL 转换为 FastDownward 规划器的内部 SAS+ 格式。换言之，它是 FastDownward 转换器的直接替代实现。与 FD 转换器相比，其执行效率显著较低，且无法从命题 PDDL 表示中自动生成有限域变量。然而，与 FD 转换器不同的是，它保留了 PDDL 输入中的所有对象流利（即 SAS+ 变量），这意味着用户可以完全控制所生成的 SAS+ 表示形式。vapo：完全可观测概率规划策略的（多种）验证器。它实际上并不验证策略是否能达成目标，而是生成在策略作用下可达的状态空间图（以 Dot 格式输出），并以策略动作标记各节点（状态）。