认知架构ACT-R的操作语义及其向约束处理规则的翻译

计算心理学旨在通过对认知过程的计算模型来解释人类认知。认知架构ACT-R因开发此类模型而广受欢迎。尽管ACT-R具有定义良好的心理学理论并已被用于解释许多认知过程，但存在两个使其认知模型难以形式化推理的问题：首先，ACT-R缺乏对其底层产生式规则系统的形式化；其次，存在许多不同的ACT-R实现与扩展，其技术构件使形式推理更加复杂。本文描述了一种形式化操作语义——极抽象语义——它尽可能多地抽象掉技术细节，从而对ACT-R理论的扩展和不同实现保持开放。在第二步中，该语义被精炼以定义许多ACT-R实现中存在的某些抽象特征——抽象语义。它聚焦于ACT-R的过程核心，并适用于对转移系统的分析，因为它仍抽象掉了诸如时序、子符号层或冲突消解等细节。此外，定义了将ACT-R模型翻译到编程语言约束处理规则（CHR）的规则。这使得抽象语义成为ACT-R的可执行规约。CHR已成功用于嵌入其他基于规则的形式体系，如图变换系统或函数式编程。已有许多结果和工具支持对CHR程序的形式推理与分析。证明了ACT-R模型到CHR的翻译相对于ACT-R的抽象操作语义是可靠且完备的。这为通过CHR分析ACT-R模型铺平了道路。因此，据我们所知，我们的抽象语义是首个同时适用于分析和执行的ACT-R表述。