An Operational Semantics for the Cognitive Architecture ACT-R and its Translation to Constraint Handling Rules

TL;DR

This paper introduces a formal operational semantics for ACT-R, enabling formal reasoning and analysis of cognitive models, and provides a translation to Constraint Handling Rules (CHR) for execution and analysis.

Contribution

It formalizes ACT-R's core using an abstract semantics and translates models into CHR, making them analyzable and executable.

Findings

The semantics abstracts from technical details, focusing on core cognitive processes.

The translation to CHR is proven sound and complete.

This is the first semantics of ACT-R suitable for analysis and execution.

Abstract

Computational psychology has the aim to explain human cognition by computational models of cognitive processes. The cognitive architecture ACT-R is popular to develop such models. Although ACT-R has a well-defined psychological theory and has been used to explain many cognitive processes, there are two problems that make it hard to reason formally about its cognitive models: First, ACT-R lacks a formalization of its underlying production rule system and secondly, there are many different implementations and extensions of ACT-R with technical artifacts complicating formal reasoning even more. This paper describes a formal operational semantics - the very abstract semantics - that abstracts from as many technical details as possible keeping it open to extensions and different implementations of the ACT-R theory. In a second step, this semantics is refined to define some of its abstract features that are found in many implementations of ACT-R - the abstract semantics. It concentrates on the procedural core of ACT-R and is suitable for analysis of the transition system since it still abstracts from details like timing, the sub-symbolic layer or conflict resolution. Furthermore, a translation of ACT-R models to the programming language Constraint Handling Rules (CHR) is defined. This makes the abstract semantics an executable specification of ACT-R. CHR has been used successfully to embed other rule-based formalisms like graph transformation systems or functional programming. There are many results and tools that support formal reasoning about and analysis of CHR programs. The translation of ACT-R models to CHR is proven sound and complete w.r.t. the abstract operational semantics of ACT-R. This paves the way to analysis of ACT-R models through CHR. Therefore, to the best of our knowledge, our abstract semantics is the first formulation of ACT-R suitable for both analysis and execution.

Tables

Table 1. Table 1. Parameters of the very abstract semantics that must be defined by the architecture or the cognitive model respectively.

Architecture		Model
$𝒞$	set of constants	$𝕋$	set of types
$𝒱$	set of variables	$\tau$	typing function
$𝔹$	set of buffers	$\Sigma$	set of rules
$A$	set of action symbols	${\sigma }_S$	start state
$\delta$	rule delay
${\rm Y}$	allowed additional information
$\circ$	chunk merging operator
$S$	rule selection function
$I$	interpretation functions
$\mathrm{𝑢𝑝𝑑𝑎𝑡𝑒}$	transformation of cognitive state after no rule transition
$\vartheta$	progress of time after no rule transition

Table 2. Table 2. Parameters of the abstract semantics that must be defined by the architecture.

Architecture
$𝒞$	set of constants
$𝒱$	set of variables
$𝔹$	set of buffers
$A$	set of action symbols
$\delta$	rule delay
${\rm Y}$	allowed additional information
$\circ$	chunk merging operator
${\mathrm{𝑟𝑒𝑞𝑢𝑒𝑠𝑡}}_b$	result of requests

Equations

$${id}_{\Delta }^{-1}(x):=\{\begin{array}{ll}c& \text{if idΔ(c)=x,}\\ \mathtt{nil}& \text{otherwise.}\end{array}$$

$${val}_x:=\{\begin{array}{ll}2& \text{if s=number}\\ 3& \text{if s=successor}\end{array}$$

$${id}_{\Delta \circ {\Delta }^{\prime }}(c):=\{\begin{array}{ll}{id}_{\Delta }(c)& \text{if c∈Δ}\\ {id}_{{\Delta }^{\prime }}(c)& \text{otherwise.}\end{array}$$

$$I(\alpha ,\sigma ):=\{(\{c\},{\gamma }^{\prime },true)\}$$

$$e\bigsqcup f:=({\Delta }^{\prime }\circ {\Delta }^{\prime \prime },\gamma ,{\upsilon }^{\prime }\wedge {\upsilon }^{\prime \prime })$$

$$\gamma (b):=\{\begin{array}{ll}{map}_{{\Delta }^{\prime },{\Delta }^{\prime \prime }}({\gamma }^{\prime }(b))& \text{if b∈dom(γ′),}\\ {map}_{{\Delta }^{\prime },{\Delta }^{\prime \prime }}({\gamma }^{\prime \prime }(b))& \text{if b∈dom(γ′′).}\end{array}$$

$$E\bigsqcup F:=\{e\bigsqcup f|e\in E\wedge f\in F\}.$$

$$I(r,\sigma )={apply}_r(\underset{\alpha \in R}{⨆}I(\alpha ,\sigma ))$$

$$\frac{(r,\theta )\in S(\sigma ),({\Delta }^{\ast },{\gamma }^{\ast },{\upsilon }^{\ast })\in I(r\theta ,\sigma )}{\sigma :=⟨\Delta ;\gamma ;\upsilon ;t⟩{\rightarrowtail }_{\mathbf{apply}}^r⟨\Delta \circ {\Delta }^{\ast };{\gamma }^{\prime };\upsilon \wedge {\upsilon }^{\ast };t^{\prime }⟩}$$

$$\frac{C(\sigma )}{\sigma :=⟨\Delta ;\gamma ;\upsilon ;t⟩{\rightarrowtail }_{\mathbf{no}}⟨\Delta ;{\gamma }^{\prime };\upsilon ;\vartheta (\sigma )⟩}$$

$$I(r,\sigma ):=\{(\{c^{\ast }\},{\gamma }^{\ast },true)\}$$

$${\gamma }^{\prime }(b):=\{\begin{array}{ll}({map}_{\Delta ,\{c^{\ast }\}}(c),d)& \text{if }{\gamma }^{\ast }(b)=(c,d)\text{ is defined}\\ ({map}_{\Delta ,\{c^{\ast }\}}(c),d\ominus \delta )& \text{otherwise, if γ(b)=(c,d).}\end{array}$$

$${\gamma }^{\prime }(b):=\{\begin{array}{ll}(c^{\ast },d)& \text{if }b=b^{\ast }\\ (c,d\ominus \delta )& \text{otherwise, if γ(b)=(c,d),}\end{array}$$

$${val}_b(s):=\{\begin{array}{ll}{id}_{\Delta }^{-1}(v)& \text{if (s,v)∈P}\\ {val}_{\gamma }(s)& \text{otherwise.}\end{array}$$

$$\frac{r⊑\sigma \wedge \theta =Bindings(r,\sigma )\wedge ({\Delta }^{\ast },{\gamma }^{\ast },{\upsilon }^{\ast })\in I(r\theta ,\sigma )}{\sigma :=⟨\Delta ;\gamma ;\upsilon ⟩{\rightarrowtail }_{\mathbf{apply}}^r⟨\Delta \circ {\Delta }^{\ast };{\gamma }^{\prime };\upsilon \wedge {\upsilon }^{\ast }⟩}$$

$${\gamma }^{\prime }(b):=\{\begin{array}{ll}({map}_{\Delta ,{\Delta }^{\ast }}(c),d)& \text{if }{\gamma }^{\ast }(b)=(c,d)\text{ is defined}\\ (c,d)& \text{otherwise, if γ(b)=(c,d).}\end{array}$$

$$\frac{\gamma (b^{\ast })=(c^{\ast },d^{\ast })\wedge d^{\ast }>0}{\sigma :=⟨\Delta ;\gamma ;\upsilon ;t⟩{\rightarrowtail }_{\mathbf{no}}⟨\Delta ;{\gamma }^{\prime };\upsilon ⟩}$$

$${\sigma }_0$$

$${\rightarrowtail }^{inc}⟨{\gamma }_2;\varnothing ;0⟩=:{\sigma }_2$$

$$r\text{enspace@}{H}_k\backslash H_r\iff G|B_c,B_b$$

$$r\text{enspace@}{H}_r\iff G|B_c,B_b.$$

$$r\text{enspace@}{H}_k\Rightarrow G|B_c,B_b.$$

$$⟨\mathbb{G};X=t\wedge \mathbb{B};\mathbb{V}⟩\equiv ⟨\mathbb{G}[X/t];X=t\wedge \mathbb{B};\mathbb{V}⟩.$$

$$⟨\mathbb{G};\mathbb{B};\mathbb{V}⟩\equiv ⟨\mathbb{G};{\mathbb{B}}^{\prime };\mathbb{V}⟩.$$

$$⟨\mathbb{G};\mathbb{B};\{X\}\cup \mathbb{V}⟩\equiv ⟨\mathbb{G};\mathbb{B};\mathbb{V}⟩.$$

$$⟨\mathbb{G};false;\mathbb{V}⟩\equiv ⟨{\mathbb{G}}^{\prime };false;{\mathbb{V}}^{\prime }⟩.$$

$$\frac{r\text{enspace@}{H}_k\backslash H_r\iff G|B_c,B_b}{[⟨H_k\uplus H_r\uplus \mathbb{G};G\wedge \mathbb{B};\mathbb{V}⟩]{\mapsto }^r[⟨H_k\uplus B_c\uplus \mathbb{G};G\wedge B_b\wedge \mathbb{B};\mathbb{V}⟩]}$$

$$[chunk({id}_{\Delta }(c),t,[[val]]):c\in \Delta \wedge c=(t,val)]$$

$$⟨$$

$$\uplus \{gamma(b,{id}_{\Delta }(c),d)|b\in \mathbb{B}\wedge \gamma (b)=(c,d)\wedge c=(t,val)\};\upsilon ;\varnothing ⟩$$

$$action(\alpha ,D,G,D_{res},C_{res},E_{res})\wedge \upsilon \leftrightarrow$$

Full text

This paper describes a formal operational semantics – the very abstract semantics – that abstracts from as many technical details as possible keeping it open to extensions and different implementations of the ACT-R theory. In a second step, this semantics is refined to define some of its abstract features that are found in many implementations of ACT-R – called the abstract semantics. It concentrates on the procedural core of ACT-R and is suitable for analysis of the general transition system since it still abstracts from details like timing, the sub-symbolic layer of ACT-R or conflict resolution.

Furthermore, a translation of ACT-R models to the declarative programming language Constraint Handling Rules (CHR) is defined. This makes the abstract semantics an executable specification of ACT-R. CHR has been used successfully to embed other rule-based formalisms like graph transformation systems or functional programming. There are many theoretical results and practical tools that support formal reasoning about and analysis of CHR programs. The translation of ACT-R models to CHR is proven sound and complete w.r.t. the abstract operational semantics of ACT-R. This paves the way to analysis of ACT-R models through CHR analysis results and tools. Therefore, to the best of our knowledge, our abstract semantics is the first abstract formulation of ACT-R suitable for both analysis and execution.

Computational cognitive modeling, ACT-R, operational semantics, source to source transformation, Constraint Handling Rules

††journalvolume: 9††journalnumber: 4††article: 39††journalyear: 2017††publicationmonth: 2††articleseq: 9††copyright: rightsretained††doi: 0000001.0000001††ccs: Theory of computation Operational semantics††ccs: Computing methodologies Cognitive science††ccs: Applied computing Psychology††ccs: Software and its engineering Constraint and logic languages††ccs: Software and its engineering Semantics

1. Introduction

Computational cognitive modeling tries to explore human cognition by building detailed computational models of cognitive processes (Sun, 2008). Cognitive architectures support the modeling process by providing a formal, well-investigated theory of cognition that allows for building cognitive models of specific tasks and cognitive features.

Currently, computational cognitive modeling architectures as well as the implementations of cognitive models are typically ad-hoc constructs. They lack a formalization from the computer science point of view. For instance, Adaptive Control of Thought – Rational (ACT-R) (Anderson et al., 2004) is a widely employed cognitive architecture. It is a modular production rule system with a special architecture of the working memory that operates on data stored as so-called chunks, i.e. the unit of knowledge in the human brain. It has a well-defined psychological theory, however, its computational system is not described formally leading to implementations that are full of technical artifacts as claimed in (Albrecht and Westphal, 2014; Stewart and West, 2007), for instance. This impedes formal reasoning about the underlying languages and the programmed models. It makes it hard to compare different implementation variants of the languages. Furthermore, it complicates verifying properties of the models. These issues call for a formal semantics of cognitive modeling languages together with proper analysis techniques.

In this paper, we describe a very abstract formulation of the operational semantics of ACT-R, called the very abstract semantics. This formalization of the fundamental parts of ACT-R is the basis for the specification of concrete implementations of the theory of the architecture, as well as for analysis of cognitive models. This very abstract semantics, extending and adapting the work of (Albrecht and Westphal, 2014), captures all possible kinds of ACT-R implementations. This can be too abstract to formally reason about actual computational models meaningfully.

Therefore, we give a concrete instance of this very abstract semantics that is suitable for analysis and implementation – the abstract semantics. It still abstracts from a variety of technical details like conflict resolution, times and latency that strongly depend on the actual implementation or even configuration of ACT-R, but includes the typical matching process of rules and some common actions that can be extended. This paves the way for computational analysis of actual cognitive models.

Eventually, we construct a sound and complete translation of ACT-R models in abstract semantics to Constraint Handling Rules (CHR). The abstract semantics is therefore directly executable via its CHR representation making it, to the best of our knowledge, the first formal operational semantics of ACT-R that is suitable for analysis and execution.

The paper is a revised and extended version of our prior work in (Gall and Frühwirth, 2015) and (Gall and Frühwirth, 2016). It has the following contributions:

1. (1)

A very abstract operational semantics of ACT-R (c.f. section 3), 2. (2)

an instance of this semantics for analysis (abstract semantics, c.f. section 4), 3. (3)

a translation of ACT-R models to the declarative programming language Constraint Handling Rules (CHR) (c.f. section 5) and 4. (4)

a soundness and completeness proof of the translation w.r.t. the operational semantics (c.f. section 6).

The formulations of the semantics (1 and 2) have been improved compared to (Gall and Frühwirth, 2015) and the translation (3) has been revised substantially compared to (Gall and Frühwirth, 2016) making it suitable for the proofs. The soundness and completeness proofs (4) have not been published before and are fundamentally new.

Constraint Handling Rules (CHR) (Frühwirth, 2009) has a formally defined operational semantics as well as a declarative semantics with corresponding soundness and completeness results. There are many theoretical and practical results and tools for analysis of CHR programs (Frühwirth, 2009). Due to its strengths in formal program analysis and its strong relation to first order (Frühwirth, 2009) and linear logic (Frühwirth, 2009; Betz and Frühwirth, 2005), it has been used as a lingua franca that embeds many rule-based approaches (Frühwirth, 2009) like term rewriting systems (Raiser and Frühwirth, 2008), graph transformation systems (Raiser, 2007; Raiser and Frühwirth, 2011) and business rules (Martin and Fages, 2007). Such embeddings have been used successfully to make the analysis results of CHR available to other approaches. The sound and complete embedding of ACT-R in CHR enables the use of these results and tools to formally reason about cognitive models.

The paper is structured as follows: We first give a short introduction to ACT-R in section 2. The formal definition of the very abstract semantics is given in section 3 and the the abstract semantics is defined as an instance in section 4. The translation scheme of abstract ACT-R models to CHR programs is described in section 5 and proven sound and complete w.r.t. the operational semantics in section 6. Related work is discussed in section 7 with a detailed comparison to prior work.

2. Description of ACT-R

In this section, we describe ACT-R informally. For a detailed introduction to the theory, we refer to (Anderson and Lebiere, 1998; Anderson et al., 2004; Taatgen et al., 2006; Anderson, 2007). Adaptive Control of Thought – Rational (ACT-R) is a popular cognitive architecture that is used in many cognitive models to describe and explain human cognition. There have been applications in language learning models (Taatgen and Anderson, 2002) or in improving human computer interaction by the predictions of a cognitive model (Byrne, 2001). The components of the ACT-R architecture even have been mapped to brain regions (Anderson, 2007, chapter 2).

Using a cognitive architecture like ACT-R simplifies the modeling process, since well-investigated psychological results have been assembled to a unified theory about fundamental parts of human cognition. In the best-case, such an architecture constrains modeling to only plausible cognitive models (Taatgen et al., 2006). Computational cognitive models are described clearly and unambiguously since they are executed by a computer producing detailed simulations of human behavior (Sun, 2008). By performing the same experiments on humans and the implemented cognitive models, the resulting data can be compared and models can be validated.

2.1. Overview of the ACT-R Architecture

The ACT-R theory is built around a modular production rule system operating on data elements called chunks. A chunk is a structure consisting of a name and a set of labeled slots that are connected to other chunks. The slots of a chunk are determined by its type. The names of the chunks are only for internal reference – the information represented by a network of chunks comes from the connections. For instance, there could be chunks representing the cognitive concepts of numbers 1, 2, … By chunks with slots number and successor we can connect the individual numbers to an ordered sequence describing the concept of natural numbers. This is illustrated in figure 1.

As shown in figure 2, ACT-R consists of modules. The goal module keeps track of the current (sub-) goal of the cognitive model. The declarative module contains declarative knowledge, i.e. factual knowledge that is represented by a network of chunks. There are also modules for interaction with the environment like the visual and the manual module. The first perceives the visual field whereas the latter controls the hands of the cognitive agent. Each module is connected to a set of buffers that can hold at most one chunk at a time.

The heart of the system is the procedural module that contains the production rules controlling the cognitive process. It only has access to a part of the declarative knowledge: the chunks that are in the buffers. A production rule matches the content of the buffers and – if applicable – executes its actions. There are three types of actions:

**Modifications: **

overwrite information in a subset of the slots of a buffer, i.e. they change the connections of a chunk.

**Requests: **

ask a module to put new information into its buffer. The request is encoded in form of a chunk. The implementation of the module defines how it reacts on a request. For instance, there are modules that only accept chunks of a certain form like the manual module that only accepts chunks that encode a movement command for the hand according to a predefined set of actions.

Nevertheless, all modules share the same interface for requests: The module receives the arguments of the request encoded as a chunk and puts its result in the requested buffer. For instance, a request to the declarative module is stated as a partial chunk and the result is a chunk from the declarative knowledge (the fact base) that matches the chunk from the request.

**Clearings: **

remove the chunk from a buffer.

The system described so far is the so-called symbolic level of ACT-R. It is similar to standard production rule systems operating on symbols (of a certain form) and matching rules that interact with buffers and modules. However, to simulate the human mind, a notion of timing, latency, priorities etc. are needed. In ACT-R, those concepts are subsumed in the sub-symbolic level. It augments the symbolic structure of the system by additional information to simulate the previously mentioned concepts.

Therefore, ACT-R has a progressing simulation time. Certain actions can take some time that depends on the information from the sub-symbolic level. For instance, chunks are mapped to an activation level that determines how long it takes the declarative module to retrieve it. Activation levels also resolve conflicts between chunks that match the same request. The value of the activation level depends on the usage of the chunk in the model (inter alia): Chunks that have been retrieved recently and often have a high activation level. Hence, the activation level changes with the simulation time. This can be used to model learning and forgetting of declarative knowledge. Similarly to the activation level of chunks, production rules have a utility that also depends on the context and the success of a production rule in prior applications. Conflicts between applicable rules are resolved by their utilities which serve as dynamic, learned rule priorities.

2.2. Syntax

We use a simplified syntax of ACT-R that we have introduced in (Gall and Frühwirth, 2015a). It is based on sets of logical terms instead of the concatenation of syntactical elements. This enables an easier access to the syntactical parts. Our syntax can be transformed directly to the original ACT-R syntax and vice-versa.

The syntax of ACT-R is defined over two possibly infinite, disjoint sets of (constant) symbols $\mathcal{C}$ and variable symbols $\mathcal{V}$. An ACT-R model consists of a set of types $\mathbb{T}$ with type definitions and a set of rules $\Sigma$. A production rule has the form $L\Rightarrow R$ where $L$ is a finite set of buffer tests and queries. A buffer test is a first-order term of the form $\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P}})$ where the buffer $b\in\mathcal{C}$ and $P\subseteq\mathcal{C}\times(\mathcal{C}\cup\mathcal{V})$ is a set of slot-value pairs $(s,v)$ where $s\in\mathcal{C}$ and $v\in\mathcal{C}\cup\mathcal{V}$. This means that only the values in the slot-value pairs can consist of both constants and variables. The right-hand side $R\subseteq\mathcal{A}$ of a rule is a finite set of actions where $\mathcal{A}=\{a(b,t,P)\enspace|\enspace a\in A,b\in\mathcal{C},t\in\mathcal{C}\mbox{ and }P\subseteq\mathcal{C}\times(\mathcal{C}\cup\mathcal{V})\}$. I.e. an action is a term of the form $a(b,t,P)$ where the functor $a$ of the action is in $A$, the set of action symbols, the first argument $b$ is a constant (denoting a buffer), the second argument is a constant $t$ denoting a type, and the last argument is a set of slot-value pairs, i.e. a pair of a constant and a constant or variable. Usually, the action symbols are defined as $A:=\{=,+,-\}$ for modifications, requests and clearings respectively. Only one action per buffer is allowed, i.e. if $a(b,t,P)\in R$ and $a^{\prime}(b^{\prime},t^{\prime},P^{\prime})\in R$, then $b\neq b^{\prime}$ (Bothell, ).

We define the function $\mathord{\mathit{vars}}$ that maps an arbitrary set of terms to its set of variables in $\mathcal{V}$. For a production rule $L\Rightarrow R$ the following must hold: $\mathord{\mathit{vars}}(R)\subseteq\mathord{\mathit{vars}}(L)$, i.e. no new variables must be introduced on the right-hand side of a rule. As we will see in the following sections about semantics, this restriction demands that all variables are bound on the left-hand side.

2.3. Informal Operational Semantics

In this section, we describe ACT-R’s operational semantics informally. The production rule system constantly checks for matching rules and applies their actions to the buffers. This means that it tests the conditions on the left hand side with the contents of the buffers (which are chunks) and applies the actions on the right hand side, i.e. modifies individual slots, requests a new chunk from a module or clears a buffer.

The left hand side of a production rule consists of buffer tests – that are terms $\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P}})$ with a buffer $b$, a type $t$ and a set of slot-value pairs $P$. The values of a slot-value pair can be either constants or variables. The test matches a buffer, if the chunk in the tested buffer $b$ has the specified type $t$ and all slot-value pairs in $P$ match the values of the chunk in $b$. Thereby, variables of the rule are bound to the actual values of the chunk. Values of a chunk in the buffers are always ground. This is ensured by the previously mentioned condition in the syntax of a rule that the right hand side of a rule does not introduce new variables (see section 2.2). Hence the chunks in the buffers stay ground.

If there is more than one matching rule, a conflict resolution mechanism that depends on the sub-symbolic layer chooses one rule that is applied. After a rule has been selected, it takes a certain time (usually 50 ms) for the rule to fire. I.e. actions are applied after this delay. During that time the procedural module is blocked and no rule can match.

The right hand side consists of actions $a(b,t,P)$, where $a\in A$ is an action symbol, $b$ is a constant denoting a buffer and $P$ is again a set of slot-value pairs. We have already explained the three types of actions (modifications, requests and clearings) roughly. In more detail, a modification overwrites only the slots specified in $P$ with the values from $P$. A request clears the requested buffer and asks a module for a new chunk. It can take some time specified by the module (and often depending on sub-symbolic values) until the request is processed and the chunk is available. During that time, other rules still can fire, i.e. requests are executed in parallel. However, a module can only process one request for a buffer at the same time. Buffer clearings simply remove the chunk from a buffer. In the following, we disregard clearings in our definitions since they are easy to add.

We now give an example rule and informally explain its behavior.

Example 2.1 (production rule).

We want to model the counting process of a little child that has just learned how to count from one to ten. We use the natural number chunks described in section 2.1 as declarative knowledge. Furthermore, we have a goal chunk of another type $g$ that memorizes the current number in a current slot. We now define a production rule, that increments the number in the counting process (and call this rule inc). We denote variables with capital letters in our examples. The left-hand side of the rule inc consists of two tests:

• •

$\texttt{=}(\mathord{\mathit{\mathord{\mathit{goal}}}},\mathord{\mathit{g}},\mathord{\mathit{\{(\mathord{\mathit{current}},X)\}}})$ and

• •

$\texttt{=}(\mathord{\mathit{\mathord{\mathit{retrieval}}}},\mathord{\mathit{\mathord{\mathit{succ}}}},\mathord{\mathit{\{(\mathord{\mathit{number}},X),(\mathord{\mathit{successor}},Y)\}}})$.

This means that the rule tests if in the goal buffer there is a chunk of type $g$ that has some number $X$ (which is a variable) in the current slot. If this number $X$ is also in the number slot of the chunk in the retrieval buffer, the test succeeds and the variable $Y$ is bound to the value in the successor slot. The actions of the rule are:

• •

$\texttt{=}(\mathord{\mathit{\mathord{\mathit{goal}}}},\mathord{\mathit{g}},\mathord{\mathit{\{(\mathord{\mathit{current}},Y)\}}})$ and

• •

$\texttt{+}(\mathord{\mathit{\mathord{\mathit{retrieval}}}},\mathord{\mathit{\mathord{\mathit{succ}}}},\mathord{\mathit{\{(\mathord{\mathit{number}},Y)\}}})$.

The first action modifies the chunk in the goal. A modification cannot change the type, that is why we just add an anonymous variable denoted by the underscore symbol in the type specification. The current slot of the goal chunk is adjusted to the successor number $Y$ and the declarative module is asked for a chunk of type $\mathord{\mathit{succ}}$ with $Y$ in its number slot. This is called a retrieval request. After a certain amount of time, the declarative module will put a chunk with $Y$ in its number and $Y+1$ in its successor slot into the retrieval buffer and the rule can be applied again.

3. Very Abstract Operational Semantics

Our goal is to define an operational semantics that captures as many ACT-R implementations as possible and leaves room for extensions and modifications. Hence, we first give them a common theoretical foundation that is based on the formalization according to (Albrecht and Westphal, 2014) – the very abstract operational semantics. It describes the fundamental concepts of a production rule system that operates on buffers and chunks like ACT-R. This work extends the definition from (Albrecht and Westphal, 2014). We compare our work with the work from (Albrecht and Westphal, 2014) in section 7.1. Later on, in section 4, we define an instance of this very abstract semantics that is suitable for analysis of cognitive models.

An ACT-R architecture is a concrete instantiation of the very abstract semantics and defines general parts of the system that are left open by the very abstract semantics like the set of possible actions $A$, the effect of such an action or the selection process. In contrast to that, an ACT-R model defines model-specific instantiations of parts like the set of types $\mathbb{T}$ and the set of rules $\Sigma$. Table 1 summarizes what is defined by the architecture and the model.

3.1. Chunk Stores

As described before in section 2, ACT-R operates on a network of typed chunks that we call a chunk store. Therefore, we first define the notion of types:

Definition 3.1 (chunk types).

A typing function $\tau:\mathbb{T}\rightarrow 2^{\mathcal{C}}$ maps each type from the set $\mathbb{T}\subseteq\mathcal{C}$ to a finite set of allowed slot names. Every type set $\mathbb{T}$ must contain a special type $\mathtt{chunk}\in\mathbb{T}$ with $\tau(\mathtt{chunk})=\emptyset$.

A chunk store is defined over a set of types and a typing function. We abstract from chunk names as they do not add any information to the system. In fact, chunks are defined as unique, immutable entities with a type and connections to other chunks:

Definition 3.2 (chunk store).

A chunk store $\Delta$ is a multi-set of tuples $(t,\mathord{\mathit{val}})$ where $t\in\mathbb{T}$ is a chunk type and $\mathord{\mathit{val}}:\tau(t)\rightarrow\Delta$ is a function that maps each slot of the chunk (determined by the type $t$) to another chunk.

Every chunk store $\Delta$ must contain a chunk $\mathtt{nil}\in\Delta$ that is defined as $\mathtt{nil}:=(\mathtt{chunk},\emptyset)$. Each chunk store $\Delta$ has a bijective identifier function $\mathord{\mathit{id}}_{\Delta}:\Delta\rightarrow\mathcal{C}$ that maps each chunk of the multi-set a unique identifier. The inverse of $\mathord{\mathit{id}}$ is defined as follows:

[TABLE]

For a chunk $c=(t,\mathord{\mathit{val}})$, the following functions are defined:

• •

$\mathord{\mathit{type}}(c)=t$ and

• •

$\mathord{\mathit{slots}}(c)=\mathord{\mathit{val}}$.

The typing function $\tau$ maps a type $t$ from the set of type names $\mathbb{T}$ to a set of allowed slots, hence the function $\mathord{\mathit{val}}$ of chunk $c$ has the slots of $c$ as domain.

Note that two chunks are only considered equivalent, if they have the same chunk identifier, type and value functions (in that case they are the indistinguishable in the multi-set and therefore treated as one and the same chunk). Hence, a chunk store can contain multiple elements with the same values that still are unique entities representing different concepts. We will see this in the following example: We model our well-known example from figure 1 as a chunk store.

Example 3.3 (chunk store of natural numbers).

The chunk store from figure 1 can be modeled as follows. Note that in the examples, we write $c{::}_{\Delta}(t,\mathord{\mathit{val}})$ to denote that the specified chunk on the right hand side has identifier $c$. When it is clear from the context, we only write ${::}$ instead of ${::}_{\Delta}$. We also use the chunk identifiers to define the connections in the slots (the $\mathord{\mathit{val}}$ functions).

• •

The set of types is $\mathbb{T}_{\ref{ex:chunk_store_nat}}=\{number,succ\}$.

• •

The typing function $\tau_{\ref{ex:chunk_store_nat}}:\mathbb{T}\to 2^{\mathcal{C}}$ is defined as $\tau_{\ref{ex:chunk_store_nat}}(\mathord{\mathit{number}})=\emptyset$ and $\tau_{\ref{ex:chunk_store_nat}}(\mathord{\mathit{succ}})=\{\mathord{\mathit{number}},\mathord{\mathit{successor}}\}$.

• •

We have the following chunks in our store $\Delta_{\ref{ex:chunk_store_nat}}$:

• –

the unique entities with identifiers $1,2,3$ that are defined as $(\mathord{\mathit{number}},\emptyset)$,

• –

$b::(\mathord{\mathit{succ}},\mathord{\mathit{val}}_{b})$ with \mathord{\mathit{val}}_{b}(s)=\begin{cases}1&\text{if s=\mathord{\mathit{number}}}\\ 2&\text{if s=\mathord{\mathit{successor}}}\end{cases}

• –

$c::(\mathord{\mathit{succ}},\mathord{\mathit{val}}_{c})$ with \mathord{\mathit{val}}_{b}(s)=\begin{cases}2&\text{if s=\mathord{\mathit{number}}}\\ 3&\text{if s=\mathord{\mathit{successor}}}\end{cases}

From the definition of a chunk store $\Delta$, we can derive a graph $(\Delta,E)$ where for each slot-value pair $\mathord{\mathit{val}}(s)=d$ of a chunk $c=(t,\mathord{\mathit{val}})\in\Delta$ there is an edge $(c,d)\in E$ with label $s$. In the graphical representation, we can label vortices with the chunk identifiers. We can apply this to our example 3.3 to derive the graph illustrated in figure 1 on page 1.

Sometimes we want to build chunk stores that only have a few chunks in them that refer to chunks in other chunk stores in their slots. We call this concept a partial chunk store.

Definition 3.4 (partial chunk store).

A partial chunk store with reference to a chunk store $\Delta$, denoted as $\Delta^{\circledcirc}$, is a multi-set of tuples $(t,\mathord{\mathit{val}})$ where $t\in\mathbb{T}$ is a chunk type and $\mathord{\mathit{val}}:\tau(t)\rightarrow\Delta\uplus\Delta^{\circledcirc}$ is a function that maps each slot of the chunk (determined by the type $t$) to another chunk from chunk store $\Delta\uplus\Delta^{\circledcirc}$. Every chunk in the partial chunk store $\Delta^{\circledcirc}$ has a unique identifier that is disjoint from the identifiers in $\Delta$. The function $\mathord{\mathit{id}}_{\Delta^{\circledcirc}}:\Delta^{\circledcirc}\rightarrow\mathcal{C}$ returns the chunk identifier for each chunk in $\Delta^{\circledcirc}$.

The set of all partial chunk stores that refer to a chunk store $\Delta$ is denoted as $\mathbf{\Delta}_{\Delta}^{\circledcirc}$.

Example 3.5 (partial chunk store).

Let $\Delta_{\ref{ex:chunk_store_nat}}$ be the chunk store from example 3.3. We define $\Delta_{\ref{ex:partial_chunk_store}}$ as a partial chunk store that refers to $\Delta_{\ref{ex:chunk_store_nat}}$. It contains the chunk $x::_{\Delta_{\ref{ex:partial_chunk_store}}}(\mathit{succ},\mathord{\mathit{val}}_{x})$ with the following slots:

[TABLE]

We define an operation that merges two (partial) chunk stores. In an abstract way it can be considered as a special multi-set union that merges two elements of a chunk store, if they have the same chunk identifiers. However, since there are many different implementations of ACT-R, we do not want to limit our formulation to this special type of multi-set union, but define a more general operator $\circ$. For the general understanding of the paper and the proofs it is sufficient to think of it as multi-set union that maintains uniqueness of chunk identifiers.

Definition 3.6 (chunk merging).

Let $\mathbf{\Delta}$ be the set of all chunk stores, $\Delta\in\mathbf{\Delta}$ a chunk store and $\mathbf{\Delta}_{\Delta}^{\circledcirc}$ the set of all partial chunk stores that refer to $\Delta$. Then $\circ:(\mathbf{\Delta}\cup\mathbf{\Delta}_{\Delta}^{\circledcirc})\times(\mathbf{\Delta}\cup\mathbf{\Delta}_{\Delta}^{\circledcirc})\rightarrow(\mathbf{\Delta}\cup\mathbf{\Delta}_{\Delta}^{\circledcirc})$ the chunk merging operator. In the following, $\Delta\subseteq\Delta^{\prime}$ denotes that every element of $\Delta$ is an element of $\Delta^{\prime}$ with preservative chunk identifiers.

We require the following properties for $\circ$. For all chunk stores $\Delta\in\mathbf{\Delta}$ and all (partial) chunk stores $\Delta^{\prime},\Delta^{\prime\prime},\Delta^{\prime\prime\prime}\in\mathbf{\Delta}\cup\mathbf{\Delta}_{\Delta}^{\circledcirc}$:

1. (1)

$(\Delta^{\prime}\circ\Delta^{\prime\prime})\circ\Delta^{\prime\prime\prime}=\Delta^{\prime}\circ(\Delta^{\prime\prime}\circ\Delta^{\prime\prime\prime})$, i.e. $\circ$ is associative. 2. (2)

$\emptyset$ is the neutral element. 3. (3)

For all $c^{\prime}\in\Delta^{\prime}$ and $c^{\prime\prime}\in\Delta^{\prime\prime}$ with $\mathord{\mathit{id}}_{\Delta^{\prime}}(c^{\prime})=\mathord{\mathit{id}}_{\Delta^{\prime\prime}}(c^{\prime\prime})$, it must hold that $c^{\prime}=c^{\prime\prime}$, i.e. both chunks have same types and value functions. 4. (4)

For all (partial) chunk stores $X\in\mathbf{\Delta}\cup\mathbf{\Delta}_{\Delta}^{\circledcirc}:$ If $X\subseteq\Delta^{\prime}$ and $X\subseteq\Delta^{\prime\prime}$, then there exist (partial) chunk stores $Y$ and $Z$ such that $\Delta^{\prime}\circ\Delta^{\prime\prime}=X\circ Y\circ Z,\Delta^{\prime}=X\circ Y$ and $\Delta^{\prime\prime}=X\circ Z$. This is a special definition of idempotency of $\circ$ for elements with the same chunk identifiers, i.e. chunks in both stores that have the same chunk identifiers, types and value functions are absorbed in the merge product.

There are the following interesting special cases:

• •

$X=\Delta^{\prime}$ leads to $\Delta^{\prime}\circ\Delta^{\prime\prime}=\Delta^{\prime}\circ Z$ with $\Delta^{\prime\prime}=\Delta^{\prime}\circ Z$, i.e. the elements of $\Delta^{\prime\prime}$ that also appear in $\Delta^{\prime}$ are absorbed in the merge product.

• •

$\Delta^{\prime}=\Delta^{\prime\prime}$ leads to $\Delta^{\prime}\circ\Delta^{\prime\prime}=\Delta^{\prime}$ with $X=\Delta^{\prime}=\Delta^{\prime\prime}$ and $Y=Z=\emptyset$. 5. (5)

If $c^{\prime}\in\Delta^{\prime}$, then $c^{\prime}\in\Delta^{\prime}\circ\Delta^{\prime\prime}$ and $\mathord{\mathit{id}}_{\Delta^{\prime}}(c^{\prime})=\mathord{\mathit{id}}_{\Delta^{\prime}\circ\Delta^{\prime\prime}}(c^{\prime})$, i.e. $\Delta^{\prime}\subseteq\Delta^{\prime}\circ\Delta^{\prime\prime}$ with preservative chunk identifiers. 6. (6)

There is a mapping $\mathord{\mathit{map}}_{\Delta^{\prime},\Delta^{\prime\prime}}:\Delta^{\prime}\uplus\Delta^{\prime\prime}\rightarrow\Delta^{\prime}\circ\Delta^{\prime\prime}$ that maps chunks from the original chunk stores to the merged chunk store. It must hold that $\mathord{\mathit{map}}_{\Delta^{\prime},\Delta^{\prime\prime}}(c)=c$ if $c\in\Delta^{\prime}$, i.e. the chunks from $\Delta^{\prime}$ remain untouched by the merging.

From the axioms it is clear that $(\mathbf{\Delta}\cup\mathbf{\Delta}_{\Delta}^{\circledcirc},\circ)$ is a monoid.

We now give two examples for possible implementations of $\circ$.

The simplest chunk merging operator would be the multi-set union that maintains uniqueness of chunk identifiers, i.e. if two chunks have the same identifiers, types and value functions, only one version will be kept in the merged store. The chunk identifiers are defined as

[TABLE]

For instance, let $\Delta:=\{c_{1},c_{2}\}$ and $\Delta^{\prime}:=\{c_{2},c_{3}\}$ with $\mathord{\mathit{id}}_{\Delta}(c_{i})=i$ for $i=1,2$ and $\mathord{\mathit{id}}_{\Delta^{\prime}}(c_{i})=i$ for $i=2,3$. We assume that $c_{i}=c_{i}$ for $i=1,2,3$, i.e. those chunks are equivalent and therefore have same types and value functions. Then $\Delta\circ\Delta^{\prime}=\{c_{1},c_{2},c_{3}\}$. Due to the same identifiers, types and value functions of the two appearances of $c_{2}$, the merged store only keeps one version of $c_{2}$ due to the idempotency axiom.

For chunk stores whose chunk identifiers have been renamed apart, this definition of $\circ$ is equivalent to real multi-set union. Therefore, $\Delta\circ\Delta^{\prime}=\Delta\uplus\Delta^{\prime}$ for all chunk stores that have disjoint chunk identifiers.

However, in most implementations chunks that have the same structure are merged to one chunk, i.e. if $c:=(t,\mathord{\mathit{val}})\in\Delta_{p}^{(\Delta)}$ and $c^{\prime}:=(t,\mathord{\mathit{val}})\in\Delta_{p^{\prime}}^{(\Delta)}$, then $c$ and $c^{\prime}$ would be merged to $c$ in $\Delta_{p}^{(\Delta)}\circ\Delta_{p^{\prime}}^{(\Delta)}$. I.e., only $c$ would be kept in the merged store. The mapping function would return $\mathord{\mathit{map}}_{\Delta_{p}^{(\Delta)},\Delta_{p^{\prime}}^{(\Delta)}}(c^{\prime})=c$.

3.2. States

We first define the individual parts of an ACT-R state. The notion of a cognitive state defines which chunks are currently in which buffer and therefore visible to the production system that can only match chunks in buffers.

Definition 3.7 (cognitive state).

A cognitive state $\gamma$ is a function $\mathbb{B}\rightarrow\Delta\times\mathbb{R}^{+}_{0}$ that maps each buffer to a chunk and a delay. The set of cognitive states is denoted as $\Gamma$, whereas $\Gamma_{\mathord{\mathrm{part}}}$ denotes the set of partial cognitive states, i.e. cognitive states that are partial functions and do not necessarily map each buffer to a chunk. We define the following functions to access the individual parts of a cognitive state $\gamma$: If $\gamma(b)=(c,d)$ for an arbitrary buffer $b$, then

• •

$\mathord{\mathit{chunk}}(\gamma(b))=c$ and

• •

$\mathord{\mathit{delay}}(\gamma(b))=d$.

The delay decides at which point in time the chunk in the buffer is available to the production system. A delay $d>0$ indicates that the chunk is not yet available to the production system. This implements delays of the processing of requests.

ACT-R adds a sub-symbolic level to the symbolic concepts that have been defined so far and that distinguish it from other production rule systems. To gather information from the sub-symbolic layer, we add the concept of (sub-symbolic) additional information that is needed to calculate sub-symbolic values. This information can be altered by an abstract function as we will see in section 3.3. The information will be expressed as multi-sets or conjunctions of predicates from first-order logic. The additional information is also used to manage data used in ACT-R’s modules.

Additionally, modules other than the procedural module hold their data in the additional information.

We now define ACT-R states as follows:

Definition 3.8 (very abstract state).

A very abstract state is a tuple $\langle\Delta;\gamma;\upsilon;t\rangle$ where $\gamma$ is a cognitive state in the sense of definition 3.7, $\upsilon$ is a multi-set of ground, atomic first order predicates (called additional information), $t\in\mathbb{R}^{+}_{0}$ is a time. The state space is denoted with $\mathcal{S}_{\mathit{va}}$.

Note that a very abstract state cannot contain variables from $\mathcal{V}$, but is only compound from terms, sets and functions over constants from $\mathcal{C}$: The chunk store $\Delta$ contains a type that is denoted by a constant and a valuation function that connects slot names (constants) to other elements from $\Delta$, the cognitive state $\gamma$ connects buffer names (constants) with chunks from $\Delta$ and a delay in $\mathbb{R}^{+}_{0}$, the additional information $\upsilon$ is a multi-set of ground, atomic predicates and the time is also a number. The set of allowed predicates for additional information is denoted as $\Upsilon$. The additional information holds data of ACT-R’s modules as well as sub-symbolic information.

We continue our running example by defining a very abstract state with one of the chunks defined in example 3.3.

Example 3.9 (ACT-R states).

We want to model the counting process of a little child that has learned the sequence of the natural numbers from one to ten as declarative facts and can retrieve those facts from declarative memory. Therefore, we add a chunk of type $g$ with a current slot that memorizes the current number in the counting process.

The following state has a chunk of type $g$ in the goal buffer that has the current number $1$. The retrieval buffer is currently retrieving the chunk $b$ with number $1$ and successor $2$. The retrieval is finished in one second as denoted by the delay. Figure 3 illustrates the state. The formal definition is:

• •

$\mathbb{T}_{\ref{ex:very_abstract_state}}=\mathbb{T}_{\ref{ex:chunk_store_nat}}\cup\{g\}$ where $\mathbb{T}_{\ref{ex:chunk_store_nat}}$ is the set of types from example 3.3.

• •

\tau_{\ref{ex:very_abstract_state}}(t)=\begin{cases}\{\mathord{\mathit{current}}\}&\text{if t=g}\\ \tau_{\ref{ex:chunk_store_nat}}(t)&\text{otherwise.}\par\end{cases}

• •

$\Delta_{\ref{ex:very_abstract_state}}=\Delta_{\ref{ex:chunk_store_nat}}\uplus\{(g,\mathord{\mathit{val}}_{\mathit{goal}})\}$ where $\mathord{\mathit{val}}_{\mathit{goal}}(\mathord{\mathit{current}})=1$.

• •

$\sigma_{0}=\langle\Delta_{\ref{ex:very_abstract_state}};\gamma_{0};\mathord{\mathit{true}};0\rangle$

• •

$\gamma_{0}(\mathord{\mathit{goal}})=((g,\mathord{\mathit{val}}_{\mathit{goal}}),0)$

• •

$\gamma_{0}(\mathord{\mathit{retrieval}})=(b,1)$ where $b$ is defined as in example 3.3.

3.3. Operational Semantics

We now define the state transition system of the very abstract semantics. As in every production rule system, we first define how matching rules are chosen. Therefore, we introduce a selection function $S$ that is defined by the architecture and maps a state to a set of matching rules and the variable bindings implied by the application of the rule.

Definition 3.10 (selection function).

Let $\Theta(\mathcal{V},\mathcal{C})$ be the set of possible substitutions over variables $\mathcal{V}$ and constants $\mathcal{C}$. A selection function is a function $S:\mathcal{S}_{\mathit{va}}\rightarrow 2^{\Sigma\times\Theta(\mathcal{V},\mathcal{C})}$ that maps a state to a set of pairs $(r,\theta)$ where $r\in\Sigma$ is a production rule and $\theta\in\Theta(\mathcal{V},\mathcal{C})$ is a substitution of variables from $\mathcal{V}$ with constants from $\mathcal{C}$, such that all variables from the rule $r$ are substituted, i.e. $\mathord{\mathit{dom}}(\theta)=\mathord{\mathit{vars}}(r)$.

For actual implementations of ACT-R, the result of $S$ is usually restricted to sets with zero or one element, but for abstract definitions there can also be more than one rule. The function $S$ usually defines a notion of matching and makes sure that only rules can fire that match visible information in the buffers, i.e. chunks that are not delayed by a time greater than zero.

To define the modification of a state by a transition, we define interpretation functions of actions that determine the possible effects of an action.

Definition 3.11 (interpretation of actions).

An interpretation of an action is a function $I:\mathcal{A}\times\mathcal{S}_{\mathit{va}}\rightarrow 2^{\mathbf{\Delta}_{\Delta}^{\circledcirc}\times\Gamma_{\mathord{\mathrm{part}}}\times\Upsilon}$. The following conditions must hold: $(\Delta^{*},\gamma^{*},\upsilon^{*})\in I(\alpha,\sigma)$ if

1. (1)

$I(\alpha,\sigma)\neq\emptyset$, i.e. the interpretation of an action has at least one effect, 2. (2)

the resulting chunk store is $\Delta^{*}$ is a partial chunk store that refers to $\Delta$ and whose chunk identifiers are disjoint from $\Delta$, 3. (3)

the co-domain of $\gamma^{*}$ is $\Delta^{*}\times\mathbb{R}_{0}^{+}$, i.e. the cognitive state can only refer to chunks in the resulting chunk store $\Delta^{*}$, and 4. (4)

if the action $\alpha$ has the buffer $b$ in its scope, i.e. $\alpha:=(b,t,p)$, then the resulting partial cognitive state $\gamma^{*}$ has only $b$ in its domain, i.e. $\mathord{\mathit{dom}}(\gamma^{*})=\{b\}$.

An interpretation maps each state and action of the form $a(b,t,P)$ – where $a\in A$ is an action symbol, $b\in\mathcal{C}$ a constant denoting a buffer, $t\in\mathcal{C}$ a type, and $P\subseteq\mathcal{C}\times(\mathcal{C}\cup\mathcal{V})$ is a set of slot-value pairs – to a tuple $(\Delta^{*},\gamma^{*},\upsilon^{*})$. Thereby, $\Delta^{*}$ is a partial chunk store that refers to $\Delta$, $\gamma^{*}$ is a partial cognitive state, i.e. a partial function that assigns only the buffer $b$ from the action to a chunk and a delay. The partial cognitive state $\gamma^{*}$ will be taken in the operational semantics to overwrite the changed buffer contents, i.e. it contains the new contents of the changed buffers. Analogously, the additional information $\upsilon^{*}$ defines the additions to the sub-symbolic level induced by the action.

Note that the interpretation of an action can return more than one possible effect. This is used in the abstract semantics where due to the lack of sub-symbolic information all possible effects have to be considered. For example, the declarative module can find more than one chunk matching the retrieval request. Usually, by comparing activation levels of chunks, one chunk will be returned. However, in the abstract semantics all matching chunks are possible. In the refined semantics, we restrict the selection to one possible effect as proposed by the ACT-R reference manual (Bothell, ).

Example 3.12 (interpretation of an action).

In this example we define an neutral effect. We will see later that if this effect is applied to a state, the state does not change modulo time.

Let $\alpha:=a(b,t,p)$ be our action that produces the neutral effect and $\sigma:=\langle\Delta;\gamma;\upsilon;t\rangle$ an ACT-R state. We define

[TABLE]

where $\gamma^{\prime}(b):=(c,d)$ for $c:=(t,\mathord{\mathit{val}})$ if $\gamma(b)=(t,\mathord{\mathit{val}})$ and some $d\in\mathbb{R}_{0}^{+}$ and undefined for all other inputs.

Intuitively, the action returns a chunk store with only one chunk $c$ that has the same type and value as the chunk $\gamma(b)$ that has been in buffer $b$ in the state $\sigma$. The resulting partial cognitive state just links $b$ to this new chunk $c$. No additional information ($\mathord{\mathit{true}}$) is added.

This is a valid interpretation, since $I(\alpha,\sigma)\neq\emptyset$, $\Delta^{*}$ is a valid partial chunk store that refers to $\Delta$. Therefore $\mathord{\mathit{val}}:\tau(t)\rightarrow\Delta$ is a valid value function. The co-domain of $\gamma^{\prime}$ is $\Delta^{*}\times\mathbb{R_{0}^{+}}$ since the co-domain of $\gamma$ is $\Delta\times\mathbb{R}_{0}^{+}$ and by definition 3.6, $\Delta\subseteq\Delta\circ\Delta^{\prime}$. Additionally, $\mathord{\mathit{dom}}(\gamma^{\prime})=\{b\}$.

To combine interpretations of all actions of a rule, we first define how two interpretations can be combined. Therefore, we introduce the following set operator, that combines two sets of sets:

Definition 3.13 (combination operator $\sqcup$ for effects).

Let $e,f$ be effects of two actions, i.e. results of an interpretation function of an action in a state $\sigma$ with chunk store $\Delta$, i.e. $e\in I(\alpha^{\prime},\sigma)$ and $f\in I(\alpha^{\prime\prime},\sigma)$. Let $e:=(\Delta^{\prime},\gamma^{\prime},\upsilon^{\prime})$ and $f:=(\Delta^{\prime\prime},\gamma^{\prime\prime},\upsilon^{\prime\prime})$ where $\Delta^{\prime},\Delta^{\prime\prime}$ are partial chunk stores with disjoint chunk identifiers that refer to $\Delta$, $\gamma^{\prime}:\mathbb{B}^{\prime}\rightarrow\Delta\circ\Delta^{\prime}\times\mathbb{R}_{0}^{+},\gamma^{\prime\prime}:\mathbb{B}^{\prime\prime}\rightarrow\Delta\circ\Delta^{\prime\prime}\times\mathbb{R}_{0}^{+}$ are partial cognitive states with disjoint domains, i.e. $\mathbb{B}^{\prime},\mathbb{B}^{\prime\prime}\subseteq\mathbb{B}$ and $\mathbb{B}^{\prime}\cap\mathbb{B}^{\prime\prime}=\emptyset$ and $\upsilon$ is a conjunction of first-order predicates. Then the combination of the effects $e$ and $f$ w.r.t. a chunk store $\Delta$ is defined as

[TABLE]

where $\gamma:\mathbb{B}^{\prime}\cup\mathbb{B}^{\prime\prime}\rightarrow(\Delta^{\prime}\circ\Delta^{\prime\prime})\times\mathbb{R}_{0}^{+}$ with

[TABLE]

The intuition behind this definition is that two effects of an action, i.e. two triples of chunk store, cognitive state and additional information, are merged to one effect that combines them. Hence, we get a merged partial cognitive state that has the combined buffer-chunk mappings of the two original cognitive states. This is possible, since the domains of the partial cognitive states are required to be disjoint.

The partial chunk stores are merged to one partial chunk store referring to the same total chunk store. Note that from the definition of $\circ$, the chunk store of the first effect is a subset of the merged store. However, the second chunk store might have lost some members. The mapping function assigns every chunk from the second store one from the merged store.

The merged additional information is a conjunction of the additional information from both effects.

The combination is well-defined: $\Delta^{\prime}\circ\Delta^{\prime\prime}$ exists since $\Delta^{\prime}$ and $\Delta^{\prime\prime}$ are partial chunk stores that refer to the same chunk store $\Delta$. Additionally, they have disjoint identifiers because they are results of an interpretation function (see definition 3.11) and therefore their merging cannot fail due to different chunks with same identifiers.

The cognitive state is valid, since it has the combined domain of $\gamma^{\prime}$ and $\gamma^{\prime\prime}$ and just maps the chunks from those original partial cognitive states to their versions in the merged chunk store by $\mathord{\mathit{map}}$, i.e. the co-domain of $\gamma$ is just the merge product of the co-domains of $\gamma^{\prime}$ and $\gamma^{\prime\prime}$ and keeps their connections of buffers to chunks.

The definition of combinations of effects can be lifted to sets of effects by the following definition. Let $E$ and $F$ be two sets of effects in some state $\sigma$ with chunk store $\Delta$, then their combination is defined as all possible pairwise combination of their elements:

[TABLE]

Since the interpretation of an action is possibly non-deterministic, i.e. might have more than one effect triple, the combination of such sets of effect triples is a set that combines each effect from the first set with each effect from the second set. This leads to a set of combined effects from which the transition system will be able to choose one non-deterministically. However, since every effect set is required to have at least one effect, it the same applies for their combination.

We now define the interpretation function $I:\Sigma\to 2^{\mathbf{\Delta}\times\Gamma_{\mathord{\mathrm{part}}}\times\Upsilon}$ that maps a rule to all its possible effects (i.e. chunk store, cognitive state and additional information).

Definition 3.14 (interpretation of rules).

In a state $\sigma:=\langle\Delta;\gamma;\upsilon;t\rangle$, a rule $r:=L\Rightarrow R$ is interpreted by an interpretation function $I:\Sigma\times\mathcal{S}_{\mathit{va}}\to 2^{\mathbf{\Delta}_{\Delta}^{\circledcirc}\times\Gamma_{\mathord{\mathrm{part}}}\times\Upsilon}$ that is defined as follows: $I(r,\sigma)$ applies the function $\mathord{\mathit{apply}}_{r}$ to all tuples in the result set when combining the individual actions of the rule:

• •

$\mathord{\mathit{apply}}:\mathbf{\Delta}_{\Delta}^{\circledcirc}\times\Gamma_{\mathord{\mathrm{part}}}\times\Upsilon\to\mathbf{\Delta}_{\Delta}^{\circledcirc}\times\Gamma_{\mathord{\mathrm{part}}}\times\Upsilon$ is a function that applies some more effects at the end of the rule application and is defined by the architecture.

• •

For all actions $\alpha\in R$, the resulting chunk stores are disjoint (i.e. chunk identifiers are renamed apart).

• •

The interpretation has the result

[TABLE]

where the combination operator $\sqcup$ refers to $\Delta$ and the $\mathord{\mathit{apply}}$ function is applied to each member of the combination set. Hence, all possible effects of the rules are combined and each of the resulting partial cognitive states is then modified by the $\mathord{\mathit{apply}}$ function that is defined by the architecture.

The $\mathord{\mathit{apply}}$ function can apply additional changes to the state that are not directly defined by its actions. For instance, it can change some sub-symbolic values that depend on the rule application like the utility of the rule itself. Note that by definition of the ACT-R syntax it is ensured that each of the $\gamma_{\mathrm{part}}$ in the combination of the individual actions is still a function, since only one action per buffer is allowed as defined in section 2.2.

It is important to mention, that there are two types of non-determinism in the interpretation of a rule:

1. (1)

The first non-determinism comes from the non-deterministic nature of interpretations of an action. Each action can lead to different results (depending on their definition). This is why all interpretation functions have power sets of effects as co-domain. 2. (2)

The second type of non-determinism comes from the definition of the combination operator that merges chunk stores by using the chunk merging operator $\circ$. Since $\circ$ is not required to be commutative, the result of the merged chunk stores may vary. This leads to possibly differing chunk identifiers. It is possible to abstract from this kind of non-determinism by introducing the concept of (graph) isomorphism on chunk stores.

We now define the operational semantics as the state transition system $(\mathcal{S}_{\mathit{va}},\rightarrowtail)$:

Definition 3.15 (very abstract operational semantics).

The transition relation $\rightarrowtail:\mathcal{S}_{\mathit{va}}\times\mathcal{S}_{\mathit{va}}$ in the very abstract operational semantics of ACT-R is defined as follows:

**Apply: **

For a rule $r$ the following transitions are possible:

[TABLE]

where

• **•: **

$\gamma^{\prime}:\mathbb{B}\rightarrow\Delta\circ\Delta^{*}$,

\gamma^{\prime}(b):=\begin{cases}(\mathord{\mathit{map}}_{\Delta,\Delta^{*}}(c),d)&\text{if }\gamma^{*}(b)=(c,d)\text{ is defined}\\ (\mathord{\mathit{map}}_{\Delta,\Delta^{*}}(c),d\ominus\delta)&\text{otherwise, if \gamma(b)=(c,d),}\end{cases}

• **•: **

x\ominus y:=\begin{cases}x-y&\text{if x>y}\\ 0&\text{otherwise}\end{cases} for two numbers $x,y\in\mathbb{R}_{0}^{+}$, and

• **•: **

$t^{\prime}=t+\delta$ for a delay $\delta\in\mathbb{R}^{+}_{0}$ defined by the concrete instantiation of ACT-R.

When applying the rule, the resulting partial chunk store $\Delta^{*}$ is merged with the chunk store $\Delta$ from the state. Hence, $\Delta\circ\Delta^{*}=\Delta\circ\Delta^{*}_{\alpha_{1}}\circ_{\Delta}\dots\circ_{\Delta}\Delta^{*}_{\alpha_{n}}$ for all actions $\alpha_{i}$ on the right-hand side of the rule. Note that $\Delta\subseteq\Delta\circ\Delta^{*}$, i.e. all chunks in $\Delta$ also appear in the merged chunk store with preservative chunk identifiers by definition 3.6 of the chunk merging.

The partial cognitive state that comes from the interpretation of the rule replaces all positions in the original cognitive state where it is defined, otherwise the original cognitive state remains untouched. Note that for all buffers $b\in\mathbb{B}$ and $b\notin\mathord{\mathit{dom}}(\gamma^{*})$ with $\gamma(b)=(c,d)$ we can also write $\gamma^{\prime}(b):=(c,d\ominus\delta)$ instead of $\gamma^{\prime}(b):=(\mathord{\mathit{map}}_{\Delta,\Delta^{*}}(c),d\ominus\delta)$ since the chunk merging guarantees that $\Delta\subseteq\Delta\circ\Delta^{*}$ with preservative identifiers as mentioned before.

The delays are taken from the partial cognitive state $\gamma^{*}$ or are reduced by a constant amount that models progression of time.

When it is clear from the context, we just use $\rightarrowtail^{r}$ to denote that the transition applies rule $r$.

**No Rule: **

[TABLE]

where

• **•: **

$C\subseteq\mathcal{S}_{\mathit{va}}$ is a side condition in form of a logical predicate,

• **•: **

$\mathord{\mathit{update}}:\mathcal{S}_{\mathit{va}}\to\Gamma_{\mathord{\mathrm{part}}}$ a function that describes how the cognitive state should be transformed,

• **•: **

$\vartheta:\mathcal{S}_{\mathit{va}}\to\mathbb{R}^{+}_{0}$ a function that describes the time adjustment in dependency of the current state, and

• **•: **

$\gamma^{\prime}(b):=\begin{cases}\mathord{\mathit{update}}(\sigma)(b)&\text{if defined}\\ \gamma(b)&\text{otherwise}\end{cases}$ is the updated state.

An apply transition applies a rule that satisfies the conditions of the selection function $S$ by overwriting the cognitive state $\gamma$ with the result from the interpretations of the actions of rule $r$. Thereby, one possible combination of all effects of the actions is considered. Note that the transition is also possible for all other combinations. Only the buffers with a new chunk are overwritten, the others keep their contents. The same applies for parameters: They keep their value except for those where $\upsilon^{*}$ defines a new value. Additionally, the rule application can take a certain time $\delta$ that is defined by the architecture. Time is forwarded by $\delta$, i.e. the time in the state is incremented by $\delta$ and the delays in the cognitive state that determine when a chunk becomes visible to the system are decremented by $\delta$ (with a minimal delay of 0).

The no rule transition defines what happens if there is no rule applicable, but there are still effects of e.g. requests that can be applied. This means that there are buffers $b\in\mathbb{B}$ with $\gamma(b)=(c,d)$ and $d>0$, i.e. information that is not visible to the production rule system. In that case there are no possible transitions in the original semantics. We generalized this case in our definition of the no rule transition that allows state transitions without rule applications. It ensures that if a side condition $C(\sigma)$ defined by the ACT-R instantiation, the cognitive state is updated according to the function $\mathord{\mathit{update}}$ and the current time of the system is set to a specified time $\vartheta(\sigma)$. Both functions are also defined by the concrete architecture. This makes new information visible to the production system and hence new rules might fire. In typical ACT-R implementations, the side condition $C(\sigma)$ is that $S(\sigma)=\emptyset$, i.e. that no rule is applicable, and $\vartheta(\sigma):=t+d^{*}$ where $\sigma$ has the time component $t$ and $d^{*}$ is the minimum delay in the cognitive state of $\sigma$. This means that time is forwarded to the minimal delay in the cognitive state and makes for instance pending requests visible to the production rule system. It can be interpreted like if the production rule system waits with the next rule application until there is new information present that leads to a rule matching the state. This behavior coincides with the specification from the ACT-R reference implementation (Bothell, ). If no transition is applicable in a state $\sigma$, i.e. there is no matching rule and no invisible information in $\sigma$, then $\sigma$ is a final state and the computation stops.

The definition of our very abstract semantics leaves parts to be defined by the actual architecture and the model. Table 1 summarizes what has to be defined by an architecture and a model.

We now show that the neutral effect from example 3.12 is a neutral element of the rule application except for the time component.

Example 3.16 (neutral element of rule applications).

Let $\sigma:=\langle\Delta;\gamma;\upsilon;t\rangle$ be an ACT-R state and $r:=L\Rightarrow\{\alpha\}$ an ACT-R rule with only one action $\alpha:=a(b^{*},t^{*},P^{*})$. Let $\gamma(b^{*}):=(t,\mathord{\mathit{val}})$.

We define $e:=I(\alpha,\sigma):=\{(\{c^{*}\},\gamma^{*},\mathord{\mathit{true}})\}$ to be the only effect of $\alpha$ where $c^{*}:=(t,\mathord{\mathit{val}})$ and $\gamma^{*}(b^{*}):=(c^{*},d^{*})$ for some $d^{*}\in\mathbb{R}_{0}^{+}$ and undefined for all other inputs. Then

[TABLE]

where $\gamma^{*}:\mathbb{B}^{\prime}\cup\mathbb{B}^{\prime\prime}\rightarrow\{c^{*}\}\times\mathbb{R}_{0}^{+}$ with

Let $\sigma\rightarrowtail^{r}\sigma^{\prime}$. Then $\sigma^{\prime}:=\langle\Delta\circ\{c^{*}\};\gamma^{\prime};\upsilon\land\mathord{\mathit{true}};t^{\prime}\rangle.$ The follow-up cognitive state $\gamma^{\prime}$ is

[TABLE]

This can be reduced to

[TABLE]

Since $c^{*}$ has the same type and value function, $\gamma^{\prime}(b)$ can be considered equivalent to $\gamma(b)$ modulo delays for all $b\in\mathbb{B}$. Hence, $\sigma$ is equivalent to $\sigma^{\prime}$ modulo delays and the time component.

4. Abstract Semantics as Instance of the Very Abstract Semantics

The abstract semantics is defined as an instance of the very abstract semantics. It is suitable for the analysis of procedural core of cognitive models because it abstracts from timings and conflict resolution by leaving parts of the transition system to non-deterministic choices and still giving room for extensions and modifications. The idea is to define the minimal core of all implementations of ACT-R’s procedural system disregarding parameter choices, timings, sub-symbolic information and module configuration. The abstract semantics captures all possible state transitions the procedural system can make.

4.1. Definition of the Abstract Semantics

Since it is a central part of the procedural system of ACT-R, we first define the notion of matchings:

Definition 4.1 (matching).

A buffer test $\beta:=\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{\mathord{\mathit{ct}}}},\mathord{\mathit{P}})$ for a buffer $b\in\mathbb{B}$ testing for a type $\mathord{\mathit{t}}\in\mathbb{T}$ and slot-value pairs $P\subseteq\mathcal{C}\times(\mathcal{C}\cup\mathcal{V})$ matches a state $\sigma:=\langle\Delta;\gamma;\upsilon;t\rangle$, written $\beta\sqsubseteq\sigma$, if and only if there is a substitution $\theta$ such that $\gamma(b)=((t,\mathord{\mathit{val}}),0)$ and for all $(s,v)\in P:\mathord{\mathit{id}}_{\Delta}(\mathord{\mathit{val}}(s))=v\theta$. We define $\mathord{\mathit{Bindings}}(\beta,\sigma):=\theta$ as the function that returns the smallest substitution that satisfies the matching $\beta\sqsubseteq\sigma$.

This definition can be extended to rules: A rule $r:=L\Rightarrow R$ matches a state $\sigma$, written as $r\sqsubseteq\sigma$, if and only if for all buffer tests $t\in L$ match $\sigma$. The function $\mathord{\mathit{Bindings}}(r,\sigma)$ returns the smallest substitution that satisfies the matching $r\sqsubseteq\sigma$.

This means that a buffer test matches a state, if the tested buffer contains a chunk of the tested type and all slot tests hold in the state, i.e. the variables in the test can be substituted by values consistently such that they match the values from the state. The values in the test are denoted by the identifiers of the chunks. Note that a test can only match chunks in the cognitive state that are visible to the system, i.e. whose delay is zero. A test cannot match chunks with a delay greater than zero.

We give the architectural parameters that are left open in the very abstract semantics:

**States: **

We set the time in every state to $t:=0$ (or any other constant) because abstract states are not timed. Hence, each abstract state is a tuple $\langle\Delta;\gamma;\upsilon;0\rangle$ where $\gamma\in\Gamma$ is a cognitive state. We sometimes project an abstract state $\langle\Delta;\gamma;\upsilon;0\rangle$ to $\langle\Delta;\gamma;\upsilon\rangle$ for the sake of brevity.

**Selection Function: **

The rule selection in the abstract semantics is simply defined as $S_{\mathit{abs}}(\sigma):=\{(r,\mathord{\mathit{Bindings}}(r,\sigma))\enspace|\enspace r\in\Sigma\wedge r\sqsubseteq\sigma\}$. Hence we select all matching rules in state $\sigma$ and replace the variables from the rules by their actual values from the matching, since in the state transition system the substitution $\theta$ is applied to the rule when calculating the effects.

**Effects: **

For a state $\sigma=\langle\Delta;\gamma;\upsilon;0\rangle$ the interpretation function $I_{\mathit{abs}}$ for actions $A:=\{\mathtt{=},\mathtt{+}\}$ in the abstract semantics is defined as follows:

• **•: **

$I_{\mathit{abs}}(=(b,t,P),\sigma)=\{(\Delta^{*},\gamma^{*},\mathord{\mathit{true}})\}$ for modifications

where

• **–: **

$c:=(t,\mathord{\mathit{val}}_{b})$,

• **–: **

$\Delta^{*}:=\{c\}$ with $\mathord{\mathit{id}}_{\Delta^{*}}(c)=i$ for a fresh id $i\in\mathcal{C}$,

• **–: **

$\gamma^{*}(b):=(c,0)$, and

• **–: **

the new slot values are:

[TABLE]

for $\gamma(b)=((t,\mathord{\mathit{val}}_{\gamma}),d)$.

This means that a modification creates a new chunk that modifies only the slots specified by $P$ and takes the remaining values from the chunk that has been in the buffer. Note that the type cannot be modified, since the resulting chunk always has the type derived from the chunk that has previously been in the buffer. Modifications are deterministic, i.e. that there is only one possible effect.

The slot-value function $\mathord{\mathit{val}}_{b}$ is well-defined, since it appears in a partial chunk store that references $\Delta$, it has $\Delta$ as co-domain by definition 3.4 of a partial chunk store.

If the action contains a slot-value pair $(s,v)$ that modifies $s$ to a chunk that was not existent in the original state $\sigma$, this chunk is not magically constructed, since we do not know its type or values. Instead, we map this slot to $\mathtt{nil}$. This comes from the definition of $\mathord{\mathit{id}}^{-1}_{\Delta}$, which is $\mathtt{nil}$ for $v$, since the chunk referenced by $v$ does not exist in $\Delta$.

• **•: **

$(\Delta^{*},\gamma^{*},\upsilon^{*})\in I_{\mathit{abs}}(+(b,t,P),\sigma)$ for requests

if

• **–: **

$\mathord{\mathit{request}}_{b}:\mathbb{T}\times 2^{\mathcal{C}\times(\mathcal{C}\cup\mathcal{V})}\times\Upsilon\to 2^{\Delta\times\mathbb{R}^{+}_{0}\times\Upsilon}$ is a function defined by the architecture for each buffer. It calculates the set of possible answers for a request that is specified by a type and a set of slot value pairs. Possible answers are tuples $(c,d,\upsilon)$ of a chunk $c$, delay $d$ and parameter valuation function $\upsilon$.

• **–: **

For all $(c^{*},d^{*},\upsilon^{*})\in\mathord{\mathit{request}}_{b}(t,P,\upsilon)$ we set \gamma^{*}(b):=\begin{cases}(c^{*},1)&\text{if d^{*}>0}\\ (c^{*},0)&\text{otherwise,}\end{cases}

and $\Delta^{*}:=\{c^{*}\}$.

Note that the additional information in the result of the request is directly added to the result of the interpretation function to update the internal state of the requested module.

• **•: **

The function $\mathord{\mathit{apply}}$ from definition 3.14 that adds additional changes to the state when a rule is applied is defined as the identity function, i.e. no changes to the state are introduced by the rule application itself but only by its actions.

**Rule Application Delay: **

The delay of a rule application is set to $\delta:=0$, since the abstract semantics does not care about timings.

**No Rule Transition: **

In the no rule transition, there are three parameters to be defined by the actual ACT-R instantiation: The side condition $C$, the state update function $\mathord{\mathit{update}}$ and the time adjustment function $\vartheta$. We define them for a state $\sigma:=\langle\gamma;\upsilon;t\rangle$ as follows:

• **•: **

$\sigma\in C$ if and only if there is a $b^{*}\in\mathbb{B}$ such that $\gamma(b^{*})=(c,d)$ with $d>0$, i.e. there is a buffer with a chunk that is not visible to the system. Those are the cases where there is a pending request. This means that the no rule transition is possible as soon as there is at least one pending request. We call the buffer of one such request $b^{*}$.

• **•: **

$\left[\mathord{\mathit{update}}(\sigma)\right](b^{*}):=(c,0)$ if $\gamma(b^{*})=(c,d)$ and $d>0$ for one $b^{*}\in\mathbb{B}$. This means that one pending request is chosen to be applied (the one appearing in $C$). Since this is a rule scheme and $b^{*}$ can be chosen arbitrarily, the transition is possible for all assignments of $b^{*}$. This coincides with the original definition of our abstract semantics where one request is chosen from the set of pending requests.

• **•: **

The function $\vartheta$ that determines how the time is adjusted after a chunk has been made visible is defined as $\vartheta(\sigma):=t$, i.e. the time is not adjusted.

Table 2 shows the parameters of the abstract semantics that have to be defined by the architecture.

We summarize the transition scheme of the abstract semantics:

**Rule transition: **

[TABLE]

where $\gamma^{\prime}:\mathbb{B}\rightarrow\Delta\circ\Delta^{*}$,

\gamma^{\prime}(b):=\begin{cases}(\mathord{\mathit{map}}_{\Delta,\Delta^{*}}(c),d)&\text{if }\gamma^{*}(b)=(c,d)\text{ is defined}\\ (\mathord{\mathit{map}}_{\Delta,\Delta^{*}}(c),d)&\text{otherwise, if \gamma(b)=(c,d).}\end{cases}

Again, since $\Delta\subseteq\Delta\circ\Delta^{*}$ with preservative chunk identifiers, we can also write

[TABLE]

**No rule transition: **

[TABLE]

where \gamma^{\prime}(b):=\begin{cases}(c^{*},0)&\text{if b=b^{*}}\\ \gamma(b)&\text{otherwise.}\end{cases}

We now extend our running example by a derivation in the abstract semantics:

Example 4.2 (abstract semantics).

We begin with the state $\sigma_{0}$ from example 3.9. It is visualized in figure 3. Then, the following derivations are possible.

[TABLE]

where

• •

$\gamma_{1}(\mathord{\mathit{retrieval}})=(b,0)$ (and $\gamma_{1}(\mathord{\mathit{goal}})=\gamma_{0}(\mathord{\mathit{goal}})$ as in $\sigma_{0}$),

• •

$\gamma_{2}(\mathord{\mathit{retrieval}})=(c,1)$ and

• •

$\gamma_{2}(\mathord{\mathit{goal}})=((g,\mathord{\mathit{val}}_{g_{2}},0)$ where $\mathord{\mathit{val}}_{g_{2}}(\mathord{\mathit{current}})=2$

In $\sigma_{0}$ no rule is applicable, but there is a pending request whose result is not visible for the production system. Hence, we can apply the no rule transition which makes the chunk $b$ visible. Then the rule inc from example 2.1 is applicable. If we assume that $\mathord{\mathit{request}}_{\mathit{retrieval}}(\mathord{\mathit{succ}},\{(\mathord{\mathit{number}},2)\},\upsilon)=(c_{\mathit{req}},1,\emptyset)$ for all additional information $\upsilon$ where $c_{\mathit{req}}=(\mathord{\mathit{succ}},\{(\mathord{\mathit{number}},2),(\mathord{\mathit{successor}},3)\})$, i.e. a chunk of type $\mathord{\mathit{succ}}$ with the number 2 in the $\mathord{\mathit{number}}$ slot and 3 in the $\mathord{\mathit{successor}}$ slot, we reach the state $\sigma_{2}$ that is illustrated in figure 4. Note that in this state again the no rule transition is possible.

5. Translation of ACT-R Models to Constraint Handling Rules

In this section we show how to translate an ACT-R model to a Constraint Handling Rules (CHR) program. This is one of the main contributions of this paper. The translation is the first that matches the current operational semantics of ACT-R. The proof of the soundness and completeness of the translation w.r.t. the abstract operational semantics of ACT-R is a new contribution of this paper.

Therefore, we first give a quick introduction to CHR and its basic concepts we need for definitions and proofs in section 5.1. Then we introduce a normal form of ACT-R rules that simplifies the translation process and proofs in section 5.2. In section 5.4 we show the translation of ACT-R states to CHR states and in section 5.5 we define the translation scheme for rules. Finally, in section 6 our translation of ACT-R models to CHR programs is proven sound and complete w.r.t. the abstract operational semantics of ACT-R.

5.1. Constraint Handling Rules (CHR)

Before we define the translation scheme of ACT-R models to CHR program, we first recapitulate syntax and semantics of CHR briefly. For an extensive introduction to CHR, its semantics, analysis and applications, we refer to (Frühwirth, 2009). We use the latest definition of the state transition system of CHR that is based on state equivalence (Raiser et al., 2009). This syntax allows for more elegant proofs and has been proven to be equivalent to the canonical so-called very abstract semantics of CHR. The definitions from those canonical sources are now reproduced. We assume the reader to be familiar with the common concepts of first-order predicate logic like predicate symbols, function symbols, predicates, functions, constants, variables, terms and formulas.

The syntax of CHR is defined over a set of variables $\mathcal{V}$, a set of function symbols (with arities) $\Phi$ and a set of predicate symbols with arities $\Pi$ that is disjointly composed of CHR constraint symbols and built-in constraint symbols. The set of constraint symbols contains at least the symbols $=/2$, $\mathord{\mathit{true}}/0$ and $\mathord{\mathit{false}}/0$.

For a constraint symbol $c/n\in\Pi$ and terms $t_{1},\dots,t_{n}$ over $\mathcal{V}$ and $\Phi$ for $1\leq i\leq n$, $c(t_{1},\dots,t_{n})$ is called a CHR constraint, if $c/n$ is a CHR constraint symbol or a built-in constraint if $c$ is a built-in constraint respectively. We now define the notion of CHR states.

Definition 5.1 (CHR state).

A CHR state is a tuple $\langle\mathbb{G};\mathbb{B};\mathbb{V}\rangle$ where the goal $\mathbb{G}$ is a multi-set of constraints, the built-in constraint store $\mathbb{B}$ is a conjunction of built-in constraints and $\mathbb{V}$ is a set of global variables.

All variables occurring in a state that are not global are called local and the local variables that are only used for built-in constraints are called strictly local variables.

CHR states can be modified by rules that together form a CHR program.

Definition 5.2 (CHR program).

A CHR program is a finite set of rules of the form

[TABLE]

where $r$ is an optional rule name, the heads $H_{k}$ and $H_{r}$ are multi-sets of CHR constraints, the guard $G$ is a conjunction of built-in constraints and the body is a multi-set of CHR constraints $B_{c}$ and a conjunction of built-in constraints $B_{b}$. Note that at most one of $H_{k}$ and $H_{r}$ can be empty. If $G$ is empty, it is interpreted as the built-in constraint $\mathord{\mathit{true}}$.

If $H_{k}=\emptyset$, the rule is called a simplification rule and we write

[TABLE]

Conversely, if $H_{r}=\emptyset$, the rule is called a propagation rule and we write

[TABLE]

Informally, a rule is applicable, if the head matches constraints from the store $\mathbb{G}$ and the guard holds, i.e. is a consequence of the built-in constraints $\mathbb{B}$. In that case, the matching constraints from $H_{k}$ are kept in the store, the constraints matching $H_{r}$ are removed and the constraints from $B_{c}$, $B_{b}$ and $G$ are added.

To define the operational semantics formally, we first have to define state equivalence over CHR states following the work in (Raiser et al., 2009). Therefore, we assume a constraint theory $\mathcal{CT}$ for the interpretation of the built-in constraints in $\Pi$.

Definition 5.3 (state equivalence of CHR states).

Equivalence between CHR states is the smallest equivalence relation $\equiv$ over CHR states that satisfies the following conditions:

**Equality as substitution: **

[TABLE]

**Transformation of the constraint store: **

If $\mathcal{CT}\models\exists\bar{s}.\mathbb{B}\leftrightarrow\exists\bar{s}^{\prime}.\mathbb{B}^{\prime}$ where $\bar{s},\bar{s}^{\prime}$ are the strictly local variables of $\mathbb{B},\mathbb{B}^{\prime}$, respectively, then:

[TABLE]

**Omission of non-occurring global variables: **

[TABLE]

**Equivalence of failed states: **

[TABLE]

The operational semantics is now defined by the following transition scheme over equivalence classes over CHR states i.e. $[\sigma]::=\{\sigma^{\prime}~{}|~{}\sigma^{\prime}\equiv\sigma\}$

Definition 5.4 (operational semantics of CHR).

For a CHR program the state transition system over CHR states and the rule transition relation $\mapsto$ is defined as the following transition scheme:

[TABLE]

Thereby, we assume that $r$ is a variant of a rule in the program such that its local variables are disjoint from the variables occurring in the representative of the pre-transition state.

We may just write $\mapsto$ instead of $\mapsto^{r}$ if the rule $r$ is clear from the context.

5.2. Set Normal Form

To simplify the translation scheme, we assume the ACT-R production rules to be in set normal form. The idea is that each buffer test contains each slot exactly once. In the general ACT-R syntax it is possible to specify more than one slot-value pair for each slot or none at all. If we assume set-normal form, we can reduce the cases to consider in the translation and soundness and completeness proofs.

We now define the set-normal form formally and show that every ACT-R production rule can be transformed to set-normal form with same semantics.

Definition 5.5 (set normal form).

An ACT-R rule $r:=L\Rightarrow R$ is in set normal form, if and only if for all buffer tests $\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P}})\in L$ and $s\in\tau(t)$ there is exactly one $v\in\mathcal{V}\cup\mathcal{C}$ such that $(s,v)\in L$.

Theorem 5.6 (set normal form).

For all ACT-R models with rules $\Sigma$, there is a set of rules $\Sigma^{\prime}$ with the following properties: For all rules $r\in\Sigma$ with $r:=L\Rightarrow R$ that are applicable in at least one state there is a rule $r^{\prime}\in\Sigma^{\prime}$ with $r^{\prime}:=L^{\prime}\Rightarrow R$ in set-normal form such that for all ACT-R states $\sigma,\sigma^{\prime}$ it holds that $\sigma\rightarrowtail^{r}\sigma^{\prime}$ if and only if $\sigma\rightarrowtail^{r^{\prime}}\sigma^{\prime}$ (in the abstract semantics).

We now give the construction of $\Sigma^{\prime}$. All rules in $\Sigma$ that are not applicable in any state do not appear in $\Sigma^{\prime}$. For all remaining rules $r\in\Sigma$, we first transform $r$ to a rule $r^{\prime}$ that is in set-normal form. For every buffer test $\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P}})\in L$ there is a test $\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P^{\prime}\theta}})\in L^{\prime}$ for a substitution $\theta$. Thereby, $P^{\prime}$ has the following slot-value pairs:

• •

For all $s\in\tau(t)$ where there is exactly one $v\in\mathcal{V}\cup\mathcal{C}$ such that $(s,v)\in P$, $(s,v)\in P^{\prime}$.

• •

For all $s\in\tau(t)$ where there is no $v\in\mathcal{V}\cup\mathcal{C}$ such that $(s,v)\in P$, there is a slot-value pair $(s,V)\in P^{\prime}$ for a fresh variable $V\in\mathcal{V}$.

• •

For all $s\in\tau(t)$ where there is are $v_{1},\dots,v_{n}\in\mathcal{V}\cup\mathcal{C}$ such that $(s,v_{i})\in P$ for $1\leq i\leq n$ we produce a substitution $\theta_{b}:=\{v_{1}/v,\dots,v_{n}\}$ and add a slot-value pair $(s,v)\in P^{\prime}$ for a $v\in\mathcal{V}\cup\mathcal{C}$. There are the following cases:

1. (1)

$v_{1},\dots,v_{n}\in\mathcal{V}:$ Then $v\in\mathcal{V}$ is a fresh variable. Intuitively, we just introduce a new variable and replace all other variables by this new variable. 2. (2)

$v_{1},\dots,v_{n}\in\mathcal{C}:$ Then $v=v_{1}$. Intuitively, since $r$ is applicable in at least one state, $v_{1}=v_{2}=\dots=v_{n}$. The slot-value pairs are redundant and therefore we only add one of them. 3. (3)

$v_{1},\dots,v_{n}\in\mathcal{V}\cup\mathcal{C}:$ W.l.o.g., $v_{1}\in\mathcal{C}$. Then $v=v_{1}$.

We define the substitution $\theta$ as the composition of all substitutions $\theta_{b}$. The rule $r^{\prime}$ is obviously in set normal form.

The proof idea is that if $r\sqsubseteq\sigma$ all variables or constants that appear in the same slot test in the same buffer have the same values. If there is a buffer test $\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P}})$ with two slot-value pairs $(s,v)\in P$ and $(s,v^{\prime})$, then $v\theta=v^{\prime}\theta$ for $\theta=\mathord{\mathit{Bindings}}(r,\sigma)$. Hence, we can replace all occurrences of $v$ and $v^{\prime}$ by $v$ and remove $(s,v^{\prime})$ from $P$. This is exactly what our construction of the set-normal form does.

5.3. Notational Aspects

We use the following symbols:

• •

Lists are denoted by enumerating their elements, e.g. $[a,b,c]$ for the list with elements $a,b$ and $c$. $[]$ denotes the empty list. We use $[H|T]$ for a list with head element $H$ and tail list $T$. We also use the following notation for list comprehension: $[x:x\in M\land p(x)]$ is the list with all elements $x$ from a (multi-)set $M$ that satisfy $p(x)$.

• •

The list concatenation is denoted with $++$.

• •

For a function $f:A\rightarrow B$ with finite domain $A$, we define $\llbracket f\rrbracket:=[(a,b):a\in A\land b\in B\land f(a)=b]$ sorted by an order on $A$ and $B$, i.e. the (sorted) enumerative list notation of the function $f$. It can be understood as the list representation of the relational representation of $f$ as a set of tuples $f\subseteq A\times B$.

5.4. Translation of States

To translate an ACT-R state to CHR, we have to define translations for the individual components of such a state.

Definition 5.7 (translation of chunk stores).

A (partial) chunk store $\Delta$ can be translated to a first order term as follows:

[TABLE]

Thereby, $\llbracket f\rrbracket$ denotes the explicit relational notation of the function $f$ as a sorted list of tuples and $[x:p(x)]$ is the list comprehension as defined in section 5.3.

We denote the translation of a (partial) chunk store $\Delta$ with $\mathord{\mathit{chr}}(\Delta)$.

Each chunk in a chunk store is translated to a term $\mathord{\mathit{chunk}}/3$ that is member of a list. Note that we do not have defined the order of chunks in the list that represents the chunk store. We consider all permutations of such chunk store lists as equivalent, since for the proofs the actual choice of order will not make any difference, since we always can choose just the translation with the “correct” order. Where necessary, we comment on that issue in our proofs in section 6. The slot-value pairs in the $\mathord{\mathit{chunk}}$ terms are sorted as defined in $\llbracket\cdot\rrbracket$.

The cognitive state $\gamma$ will be represented by $\mathord{\mathit{gamma}}/3$ constraints that map a buffer $b\in\mathbb{B}$ to a chunk identifier and a delay. Since additional information is already represented as logical predicates, we represent them as built-in constraints in the CHR store. We can now define the translation of an abstract state.

Definition 5.8 (translation of abstract states).

An abstract ACT-R state $\sigma:=\langle\Delta;\gamma;\upsilon\rangle$ can be translated to the following CHR state:

[TABLE]

We denote the translation of an ACT-R state $\sigma$ by $\mathord{\mathit{chr}}(\sigma)$.

The chunk store is represented by a $\mathord{\mathit{delta}}$ constraint that contains the translated chunk store as defined in definition 5.7. Hence, a valid translation of an ACT-R state can only contain exactly one $\mathord{\mathit{delta}}$ constraint.

For every buffer of the given architecture, a constraint $\mathord{\mathit{gamma}}$ with buffer name, chunk id and delay is added to the state. Since $\gamma$ is a total function, every buffer has exactly one $\mathord{\mathit{gamma}}$ constraint. Additionally, the chunk id in the $\mathord{\mathit{gamma}}$ constraint must appear in exactly one $\mathord{\mathit{chunk}}$ constraint because the co-domain of gamma refers to $\Delta$ and the chunk ids are unique.

Additional information is used directly as built-in constraints.

5.5. Translation of Rules

In our translation scheme, ACT-R rules are translated to corresponding CHR rules.

5.5.1. Auxiliary Functions for Variable Names

To manage relations between newly introduced variables, we define some auxiliary functions. The functions all produce variable names from the set of variables $\mathcal{V}$ for a set of arguments that are from the set of constants $\mathcal{C}$ (or a subset of it) and are applied during the translation, i.e. they do not appear in the generated CHR code.

Definition 5.9 (variable functions).

Let $\mathcal{V},\mathcal{C}$ be the set of variables and constants of an ACT-R architecture respectively, $\mathbb{B}\subset\mathcal{C}$ the set of buffers of this architecture and $\mathcal{V}_{i}\subset\mathcal{V}$ for $i=1,\dots,6$ are disjoint subsets of the set of variables. Then the following auxiliary functions are defined:

**Chunk variable function: **

$\mathord{\mathit{cvar}}:\mathbb{B}\rightarrow\mathcal{V}_{1},b\mapsto C^{1}_{b}$ that returns a fresh, unique variable $C^{1}_{b}$ for each buffer $b$. It identifies the chunk of a particular buffer in the translation.

**Result variable functions: **

$\mathord{\mathit{resstore}},\mathord{\mathit{resid}},\mathord{\mathit{resdelay}}:\mathbb{B}\rightarrow\mathcal{V}_{i}$ for $i=2,3,4$ are defined as $b\mapsto C^{i}_{b}$ and return a fresh, unique variable $C^{i}_{b}$ for each buffer $b$. They are needed to memorize the results of an action.

**Merge variable function: **

$\mathord{\mathit{mergeid}}:\mathbb{B}\times\mathcal{V}_{5},(b,s)\mapsto V_{b,s}$ that returns a fresh, unique variable $C^{6}_{b}$ for each buffer $b$. It is needed to memorize the new chunk identifier after merging the chunk in $b$ with the existing chunk store.

**Cognitive state variable function: **

$\mathord{\mathit{cogstate}}:2^{\mathbb{B}}\rightarrow 2^{\mathbb{B}\times\mathcal{V}_{6}},\mathord{\mathit{cogstate}}(B)\mapsto[(b,V_{b})~{}:~{}b\in B\land V_{b}\in\mathcal{V}_{6}]$ (where the list is sorted by the $b$). The function returns a set of buffer-variable pairs for a set of buffers. From $\mathord{\mathit{cogstate}}(\mathbb{B})=\llbracket\gamma\rrbracket$ it follows that $V_{b}=\gamma(b)$, i.e. $\mathord{\mathit{cogstate}}(\mathbb{B})$ can be considered as a pattern for the cognitive state.

5.5.2. Built-in Constraints for Actions

We define some built-in constraints that are needed for the translation. The idea is that they calculate the results of actions, chunk merging and chunk mapping as defined in the operational semantics of ACT-R. For actual instantiations of the abstract semantics (i.e. with a defined set of actions and chunk merging and mapping mechanisms), it has to be shown that their CHR implementations obey the properties that we define in the following.

Definition 5.10 (action built-ins).

Let $\alpha:=a(b,t,P)$ be an action and $\sigma:=\langle\Delta;\gamma;\upsilon\rangle$ an ACT-R state. Let $D:=\mathord{\mathit{chr}}(\Delta)$ be the CHR representation of the chunk store in $\sigma$ and $G:=\llbracket\gamma\rrbracket$ be the enumerative list representation of the cognitive state $\gamma$.

For all $\Delta^{*},\gamma^{*},\upsilon^{*}$: If $(\Delta^{*},\gamma^{*},\upsilon^{*})\in I(\alpha,\sigma)$ is the result of the interpretation of $\alpha$ in $\sigma$ with $\gamma^{*}(b):=(c_{b}^{*},d_{b}^{*})$, the built-in constraint $\mathord{\mathit{action}}/6$ is defined as follows:

[TABLE]

Intuitively, the $\mathord{\mathit{action}}$ built-in constraint represents a function that gets the action $\alpha$, CHR representations of the constraint store $\Delta$ and the cognitive state $\gamma$ as input and returns by the help of the additional information $\upsilon$ the CHR representation of $I(\alpha,\sigma)$. The constraint theory of the $\mathord{\mathit{action}}$ constraint is well-defined, since in definition 3.11, $\gamma^{*}$ has the domain $\{b\}$ and co-domain $\Delta^{*}\times\mathbb{R}_{0}^{+}$, hence $\gamma^{*}(b)$ is defined. Since $c_{b}^{*}\in\Delta^{*}$, $\mathord{\mathit{id}}_{\Delta^{*}}(c_{b}^{*})$ is defined.

5.5.3. Built-in Constraints for Chunk Merging

In the abstract semantics, chunk stores are merged by the operator $\circ$. In the following, built-in constraints are defined that implement $\circ$ and the corresponding mapping function $\mathord{\mathit{map}}$.

Definition 5.11 (merge built-in).

For a set of chunk stores $\{\Delta_{1},\dots,\Delta_{n}\}$ with $D_{i}:=\mathord{\mathit{chr}}(\Delta_{i})$ for $i=1,\dots,n$, the built-in $\mathord{\mathit{merge}}/2$ is defined as follows:

[TABLE]

Definition 5.12 (map built-in).

For two CHR representations of chunk stores $D:=\mathord{\mathit{chr}}(\Delta)$ and $D^{\prime}:=\mathord{\mathit{chr}}(\Delta^{\prime})$, the built-in constraint $\mathord{\mathit{map}}/4$ is defined as:

[TABLE]

The main difference to the definition of the function $\mathord{\mathit{map}}$ from the abstract semantics is that the built-in constraint operates on chunk identifiers whereas the function operates directly on chunks. Note that in the case that the chunk with identifier $C$ appears in neither in $D$ nor in $D^{\prime}$, $C^{\prime}$ is bound to $\mathtt{nil}$ by definition of $\mathord{\mathit{id}}$ (see definition 3.2).

5.5.4. List Operations

We use the built-in constraint $\mathord{\mathit{in}}/2$ to denote that a term is member of a list.

Definition 5.13 (member of a list).

For a term $c$ and a list $l$, the constraint $c~{}\mathord{\mathit{in}}~{}l$ holds, iff there is a term $c^{\prime}$ that is member of $l$ and $c=c^{\prime}$.

Note that variables in $c$ are bound to the values in $l$ by this definition.

5.5.5. Translation Scheme for Rules

We can now define the translation scheme for rules.

Definition 5.14 (translation of rules).

An ACT-R rule in set-normal form $r:=L\Rightarrow R$ can be translated to a CHR rule of the following form:

[TABLE]

Note that ACT-R constants and variables from $\mathcal{C}$ and $\mathcal{V}$ are implicitly translated to corresponding CHR variables.

We denote the translation of a rule $r$ by $\mathord{\mathit{chr}}(r)$ and the translation of an ACT-R model $\Sigma$ that is a set of ACT-R rules by $\mathord{\mathit{chr}}(\Sigma)$. Thereby, $\mathord{\mathit{chr}}(\Sigma):=\{\mathord{\mathit{chr}}(r)~{}|~{}r\in\Sigma\}.$

The intuition behind the translation can be described as follows:

The CHR rule tests the state for a $\mathord{\mathit{delta}}/1$ constraint representing the chunk store and $\mathord{\mathit{gamma}}/3$ constraints that come from the buffer tests of the rule. In the $\mathord{\mathit{gamma}}/3$ constraints a variable for the chunk identifier is introduced. In the guard, the built-in constraint $\mathord{\mathit{in}}/2$ checks, if the chunk store represented as a list contains a term $\mathord{\mathit{chunk}}/3$ with the same type and slot-value pairs as specified in the buffer tests. The connection to the buffer is realized by the same variable for the chunk identifier (through the variable function $\mathord{\mathit{cvar}}$). Since the rule is in set-normal form, the buffer tests are already completed (i.e. all slots are tested) and represented as a sorted list of slot-value pairs as in the state.

In the body of the rule, the built-in constraint calculates the result of each action from the right-hand side of the ACT-R rule. The resulting chunk stores are merged to one store $D^{\prime}$ by the built-in constraint $\mathord{\mathit{merge}}$. Note that the order of merging is not specified by the translation scheme (as it is not specified by the ACT-R abstract semantics).

The built-in constraint $\mathord{\mathit{map}}/4$ implements the $\mathord{\mathit{map}}$ function of the ACT-R semantics and gives access to the possibly modified chunk identifier of all elements in $D^{\prime}$. By definition of $\mathord{\mathit{map}}$, only chunk identifiers in $D^{\prime}$ are modified by merging. The resulting chunk identifiers are bound to a variable specified by the variable function $\mathord{\mathit{mergeid}}/1$.

The resulting chunk store $\mathord{\mathit{delta}}$ and $\mathord{\mathit{gamma}}$ constraints for all buffers are added. If the buffers have been modified, the $\mathord{\mathit{gamma}}$ constraints points to the resulting chunk of the action, if not it shows to the chunk that has been in the buffer before.

5.6. No Rule Transition

In addition to transitions by rule applications, ACT-R can also have state transitions without rule applications. This is useful for instance, if no rule is applicable (i.e. computation is stuck in a state) but there are pending requests, then simulation time can be forwarded to the point where the next request is finished and its results are visible to the procedural system. This may trigger new rules and continue the computation.

The no rule transition can be modeled in CHR by one individual generic rule:

[TABLE]

This transition is possible for all requests that are pending (i.e. that have a delay $D>0$). Hence, the system chooses one request non-deterministically.

6. Soundness and Completeness of the Translation

In this section, we show that our translation is sound and complete w.r.t. the abstract semantics of ACT-R. This means that every transition that is possible in the abstract ACT-R semantics is also possible in CHR and vice versa.

The first step is to show that the results of the built-in constraints in the body of a translated ACT-R rule are equivalent to the interpretation of the right-hand side of the ACT-R rule. Therefore, we use that by definition the built-in constraints $\mathord{\mathit{action}},\mathord{\mathit{merge}}$ and $\mathord{\mathit{map}}$ are equivalent to their ACT-R counterparts. Additionally, we have to show that the combination of the results of individual actions leads to the same result as the built-in constraints. We use induction to show that in the following lemma.

Lemma 6.1 (equivalence of effects).

For an ACT-R rule $r:=L\Rightarrow R$ in set-normal form, a state $\sigma:=\langle\Delta,\gamma,\upsilon,t\rangle$ and $D=\mathord{\mathit{chr}}(\Delta)$. Let $I(r,\sigma):=(\Delta^{*},\gamma^{*},\upsilon^{*})$ with $\bigwedge_{b\in\mathord{\mathit{dom}}(\gamma^{*})}\gamma^{*}(b)=(c_{b}^{*},d_{b}^{*})$. Then the following two propositions are equivalent:

1. (1)

[TABLE] 2. (2)

[TABLE]

Proof.

We use induction over the number of actions in $R$.

**base case: $|R|=1$: **

Let $r:=L\Rightarrow R$ be an ACT-R rule in set-normal form with one action $\alpha\in R$ and $\sigma:=\langle\Delta,\gamma,\upsilon,t\rangle$. Let $D=\mathord{\mathit{chr}}(\Delta)$ and $G=\llbracket\gamma\rrbracket$. Let $I(r,\sigma):=(\Delta^{*},\gamma^{*},\upsilon^{*})$ with $\bigwedge_{b\in\mathord{\mathit{dom}}(\gamma^{*})}\gamma^{*}(b)=(c_{b},d_{b})$ and $I(\alpha,\sigma):=(\Delta_{\alpha},\gamma_{\alpha},\upsilon_{\alpha})$ with $(c_{\alpha},d_{\alpha})=\gamma_{\alpha}(b)$.

We start with

[TABLE]

First of all, we reduce the $\mathord{\mathit{action}}$ constraint by use of definition 5.10:

[TABLE]

By definition 5.11, we can reduce the $\mathord{\mathit{merge}}$ constraints to

[TABLE]

which is by definition of $D:=\mathord{\mathit{chr}}(\Delta)$ from the assumptions and $D_{\mathit{res}}=\mathord{\mathit{chr}}(\Delta_{\alpha})$ from the last step equivalent to

[TABLE]

Since $C_{\mathit{res}}=\mathord{\mathit{id}}_{\Delta_{\alpha}}(c_{\alpha})$ and therefore a $\mathord{\mathit{chunk}}$ term with identifier $C_{\mathit{res}}$ appears in $D^{*}$ (and not in $D$), we can now reduce the $\mathord{\mathit{map}}$ built-in by definition 5.12 and get together with the definitions of $D$ and $D^{*}$ to

[TABLE]

Since we have that $C_{\mathit{res}}=\mathord{\mathit{id}}_{\Delta_{\alpha}}(c_{\alpha})$, this is equivalent to

[TABLE]

By definition 3.14, we have that for one action $\Delta_{\alpha}=\Delta^{*}$ and $c_{\alpha}=c^{*}$. Hence, this is equivalent to

[TABLE]

All in all, this proves the proposition for $|R|=1$.

**induction step: $|R|\rightarrow|R|+1$: **

Let $\sigma:=\langle\Delta;\gamma;\upsilon\rangle$ be an ACT-R state and $D:=\mathord{\mathit{chr}}(\Delta)$ the CHR representation of the chunk store and $G:=\llbracket\gamma\rrbracket$ the enumerative list representation of the cognitive state.

Let $r^{\prime}:=L\Rightarrow R^{\prime}$ with $R^{\prime}:=R\cup\alpha$ be a rule that has been constructed from a rule $r:=L\Rightarrow R$. Let $I(r,\sigma):=(\Delta^{*},\gamma^{*},\upsilon^{*})$ with $\bigwedge_{b\in\mathord{\mathit{dom}}(\gamma^{*})}\gamma^{*}(b)=(c_{b}^{*},d_{b}^{*})$ be the interpretation of the smaller rule $r$ with $|R|$ actions.

Let $I(r^{\prime},\sigma):=(\Delta^{**},\gamma^{**},\upsilon^{**})$ with $\bigwedge_{b\in\mathord{\mathit{dom}}(\gamma^{**})}\gamma^{**}(b)=(c_{b}^{**},d_{b}^{**})$ be the interpretation of the rule $r^{\prime}$ that has $|R|+1$ actions..

We begin with

[TABLE]

We need to apply the induction hypothesis. Therefore, we split the conjunctions and lists and get the equivalent formula

[TABLE]

By definition 5.10 of $\mathord{\mathit{merge}}$ and associativity of $\circ$ and neutral element $[]=\mathord{\mathit{chr}}(\emptyset)$, we can split the merging as follows: We first merge the actions in $R$ to $D^{*}$ and then merge $D^{*}$ with the result chunk of action $\alpha$ to $D^{**}$:

[TABLE]

We can now introduce an intermediate result chunk store that merges the original store $D$ with the results from $r$, i.e. $D^{*}$, to a chunk store $D^{\prime}$. We introduce some auxiliary variables $C_{b}^{\prime}$ that map the chunk identifiers of the intermediate chunk store $D^{*}$ to the resulting chunk store $D^{*}$:

[TABLE]

We can now apply the induction hypothesis:

[TABLE]

Thereby, it holds by definition of $I(r,\sigma)$ that $\mathord{\mathit{dom}}(\gamma^{*})=\{b~{}|~{}\alpha_{b}\in R\}$.

If we apply definition 5.10 to the remaining $\mathord{\mathit{action}}$ constraint of action $\alpha$, we get

[TABLE]

Hence, we have that

[TABLE]

Thus, $D^{**}$ is the CHR version of the merging of the results from the actions in $R$ merged with the results from $\alpha$. By definition 3.14 of the interpretation of rules, we have that

[TABLE]

This is equivalent to

[TABLE]

by definition of $r,r^{\prime}$ and the interpretation of rules (definition 3.14).

We now reduce the last $\mathord{\mathit{merge}}$ constraint to:

[TABLE]

We can now reconnect the $\mathord{\mathit{map}}$ constraints and get

[TABLE]

By definition 3.15, for all defined buffers $\gamma^{**}(b)=\mathord{\mathit{map}}_{\Delta,\Delta^{**}}(c_{b})$ and we have assumed that $\gamma^{**}(b)=c_{b}^{**}$. By definition 5.12, this yields

[TABLE]

. $\mathord{\mathit{id}}_{\Delta^{**}}^{-1}(C_{b})$ exists, since the co-domain of $\gamma^{**}$ is $\Delta^{**}\times\mathbb{R}^{+}_{0}$ by definition 3.4 and the $C_{b}$ are identifiers for the chunks in $\gamma^{**}$.

If we apply all this to the conjunction in $(*)$, we get

[TABLE]

∎

The next lemma proves that rule application transitions are sound.

Lemma 6.2 (soundness of rule applications).

For all ACT-R rules $r$ and ACT-R states $\sigma,\sigma^{\prime}\in\mathcal{S}_{\mathit{abs}}:$ if $\sigma\rightarrowtail^{r}\sigma^{\prime}$ then $\mathord{\mathit{chr}}(\sigma)\mapsto^{r}\mathord{\mathit{chr}}(\sigma^{\prime})$.

Proof.

Let $r:=L\Rightarrow R$ and $\sigma:=\langle\Delta;\gamma;\upsilon;0\rangle$. Since $r\sqsubseteq\sigma$, we know that for every buffer test $\beta:=\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P}})$ there is a substitution $\theta$ such that $\gamma(b)=((t,\mathord{\mathit{val}}),0)$ and for all $(s,v)\in P:\mathord{\mathit{id}}_{\Delta}(\mathord{\mathit{val}}(s))=v\theta$.

Let $\rho:=\mathord{\mathit{chr}}(\sigma)$ the CHR translation of the ACT-R state $\sigma$. By definition 5.8, we have that

[TABLE]

In the next step we split the state to only concentrate on the parts we are interested in for the rule application, i.e. $\mathord{\mathit{gamma}}$ constraints for buffers that occur in a test. We do the same by splitting the representation of the constraint store to the chunks that occur in buffers and all other chunks. This is possible, since $\mathord{\mathit{chr}}(\Delta)$ does not define an order on the $\mathord{\mathit{chunk}}$ terms in the list in the $\mathord{\mathit{delta}}$ constraint.

[TABLE]

Note that by now we only have rewritten the CHR state without requiring that the tests we refer to match.

Due to the fact that $r\sqsubseteq\sigma$, we can apply this knowledge to the translated state:

[TABLE]

Since $r$ is in set-normal form, we can assume that there is only one test for each buffer in $L$. Hence, we find a $\mathord{\mathit{gamma}}$ constraint in $\rho$ for each such test without violating definition 5.8, that only produces one $\mathord{\mathit{gamma}}$ constraint for each buffer.

Due to set-normal form of $r$ and hence totality of $P$ w.r.t. the domain of $\mathord{\mathit{val}}$, it is clear that $P\theta=\llbracket\mathord{\mathit{val}}\rrbracket$. Hence, we can reduce the state to:

[TABLE]

We introduce a substitution with fresh variables to replace the chunk identifiers in the state, i.e. $\theta^{\prime}:=\{\mathord{\mathit{cvar}}(b)/\mathord{\mathit{id}}_{\Delta}(c)~{}|~{}\gamma(b)=c\}$.

[TABLE]

Let $\Theta$ be the conjunction of syntactic equality constraints that can be derived from the substitution $\theta\cup\theta^{\prime}$, i.e. each substitution $x/t\in\theta\cup\theta^{\prime}$ appears in $\Theta$ as $x=t$. By definition **Equality as substitution: **, we can move the substitution to the built-in store:

[TABLE]

We introduce a fresh variable $D$ and add $D{=}[\mathord{\mathit{chunk}}(\mathord{\mathit{cvar}}(b),t,P)~{}:~{}\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P}})\in L]{++}\mathbb{D}$ to the built-in store, which leads to the equivalent state:

[TABLE]

By definition 5.13, we have that $D{=}d\leftrightarrow\{\mathord{\mathit{chunk}}(\mathord{\mathit{cvar}}(b),t,P)~{}\mathord{\mathit{in}}~{}D~{}|~{}\texttt{=}(\mathord{\mathit{b}},\mathord{\mathit{t}},\mathord{\mathit{P}})\}$. We can replace the corresponding built-ins by definition **Transformation of the constraint store: **:

[TABLE]

Let $\mathord{\mathit{chr}}(r):=H\Leftrightarrow G~{}|~{}B_{c},B_{b}$. By definition 5.14, we have that

[TABLE]

By definition 5.4, $\mathord{\mathit{chr}}(r)$ is applicable in $\rho\equiv\mathord{\mathit{chr}}(\sigma)$ and $\rho\mapsto^{r}\rho^{\prime}$ with

[TABLE]

Due to the definition 5.14 of $\mathord{\mathit{chr}}(r)$, we have that

[TABLE]

Since $r$ is in set-normal form, all buffers appearing in $L$ also appear in $R$. Hence, all $\mathord{\mathit{gamma}}$ constraints removed by $\mathord{\mathit{chr}}(r)$ are added in $B_{c}$. There is exactly one $\mathord{\mathit{delta}}$ constraint in $\rho^{\prime}$. It remains to show that the $\mathord{\mathit{delta}}$ and $\mathord{\mathit{gamma}}$ constraints are the ones describing the state $\sigma^{\prime}$.

By lemma 6.1, we have that for all $I(r,\sigma)\ni(\Delta^{*},\gamma^{*},\upsilon^{*})$ with $\gamma^{*}(b)=(c_{b}^{*},d_{b}^{*})$ for all $b\in\mathord{\mathit{dom}}(\gamma^{*})$

[TABLE]

All in all, we get by definition 5.8 that $\rho^{\prime}\equiv\mathord{\mathit{chr}}(\sigma^{\prime})$. Hence, the translation of rule applications is sound w.r.t. the abstract operational semantics of ACT-R. ∎

We have now shown that our translation is sound regarding rule applications, i.e. a rule that can be applied in the abstract semantics of ACT-R can also be applied in the translated CHR program and leads to the same result. The state transition system of ACT-R has a second type of transitions: the no-rule transitions, that can be applied if there is a buffer with a delay $>0$, i.e. an invisible chunk. In that case, the no-rule transition allows us to make this chunk visible to the production system by setting the delay to zero. We now show that our translation is sound and complete regarding the no-rule transition.

Lemma 6.3 (soundness and completeness of the no-rule transition).

For an ACT-R model $M$, ACT-R states $\sigma$ and $\sigma^{\prime}$ and their CHR counterparts $\mathord{\mathit{chr}}(M),\mathord{\mathit{chr}}(\sigma)$ and $\mathord{\mathit{chr}}(\sigma^{\prime})$ the following propositions are equivalent:

1. (1)

$\sigma\rightarrowtail_{\mathbf{no}}\sigma^{\prime}$* in the model $M$* 2. (2)

$\mathord{\mathit{chr}}(\sigma)\mapsto^{\mathit{no}}\mathord{\mathit{chr}}(\sigma^{\prime})$**

Proof.

We start with proposition 1. Let $\sigma:=\langle\Delta;\gamma;\upsilon\rangle$ and $\sigma^{\prime}:=\langle\Delta;\gamma^{\prime};\upsilon\rangle$. In the abstract semantics, the no-rule transition is defined as

[TABLE]

where \gamma^{\prime}(b)=\begin{cases}(c^{*},0)&\text{if b=b^{*},}\\ \gamma(b)&\text{otherwise.}\end{cases}

The no-rule transition in CHR is represented by the following CHR rule in $\mathord{\mathit{chr}}(M)$:

[TABLE]

Since the no-rule transition is applicable in $\sigma$ for some arbitrary but fixed $b^{*}$, it holds that

[TABLE]

Therefore, in $\mathord{\mathit{chr}}(\sigma)$ there must have the following form by definition 5.8:

[TABLE]

Since $d^{*}>0$, this is equivalent to

[TABLE]

and therefore the rule no can be applied to $\mathord{\mathit{chr}}(\sigma)$ by definition 5.4. This leads to the state $\rho^{\prime}$ with

[TABLE]

By definition 5.8, we have that $\rho^{\prime}\equiv\mathord{\mathit{chr}}(\sigma)$.

The other direction is analogous. ∎

Lemma 6.4 (completeness of rule applications).

Let $\rho,\rho^{\prime}$ be CHR states that have been translated from ACT-R states, i.e. there are ACT-R states $\sigma,\sigma^{\prime}$ such that $\rho:=\mathord{\mathit{chr}}(\sigma)$ and $\rho^{\prime}:=\mathord{\mathit{chr}}(\sigma^{\prime})$. Let $r$ be a CHR rule translated from an ACT-R rule $s$. If $\rho\mapsto_{r}\rho^{\prime}$ then $\sigma\rightarrowtail_{s}\sigma^{\prime}$.

Proof.

The CHR rule $r:=H\Leftrightarrow G~{}|~{}B_{c},B_{b}$ has been translated from an ACT-R rule $s$. Let $s:=L\Rightarrow R$ be an ACT-R rule in set normal form. Then $r$ has the following form by definition 5.14:

[TABLE]

where $B_{b}$ are the built-in constraints of the body and $B_{c}$ the CHR constraints.

Since $r$ is applicable in $\rho$, by definition 5.4, $\rho$ must have the following form:

[TABLE]

Thereby, $\mathbb{G}$ is a multi-set of user-defined constraints and $\mathbb{C}$ a conjunction of built-in constraints. Since by definition of ACT-R states, $H\uplus\mathbb{G}$ must be ground and therefore there must be some built-in constraints $\Theta$ in $\mathbb{C}$ that bind those variables to the values from the state:

[TABLE]

$\Theta$ is a conjunction of constraints of the form $V=c$ for a variable $V$ and a term $c$, that binds the variables from $H$ and $G$ to the values from the state, i.e. the variables $\mathord{\mathit{cvar}}(b),\mathord{\mathit{dvar}}(b)$ (for all $b\in\mathbb{B}$) and the variables appearing in the $P$ from the guard are bound to some values from the state. We denote $\theta$ as the substitution that follows from $\Theta$. Furthermore, $\rho$ must contain the additional information $\upsilon$:

[TABLE]

We now want to construct the ACT-R state $\sigma$. Let $\sigma:=\langle\Delta;\gamma;\upsilon^{\prime}\rangle$. Thereby, $\mathord{\mathit{chr}}(\Delta)=D$ and for all $b\in\mathbb{B}:\gamma(b)=(\mathord{\mathit{id}}_{\Delta}^{-1}(\mathord{\mathit{cvar}}(b)),\mathord{\mathit{dvar}}(b))\theta$ by definition 5.8. Additionally, $\upsilon^{\prime}:=\upsilon$. We can now apply the same equivalences as in lemma 6.2 in reverse order and get

[TABLE]

From there it is clear that $s\sqsubseteq\sigma$ by definition 4.1. We now apply $s$ to $\sigma$ according to definition 3.15 and get

[TABLE]

where $(\Delta^{*},\gamma^{*},\upsilon^{*})\in I(s\theta,\sigma)$ and \gamma^{\prime}(b):=\begin{cases}(\mathord{\mathit{map}}_{\Delta,\Delta^{*}}(c),d)&\text{if }\gamma^{*}(b)=(c,d)\text{ is defined}\\ (\mathord{\mathit{map}}_{\Delta,\Delta^{*}}(c),d)&\text{otherwise, if \gamma(b)=(c,d).}\end{cases}

By definition 5.4, the application of $r$ in $\rho$ leads to the state $\rho^{\prime}$ with

[TABLE]

By lemma 6.1, we get that $B_{b}$ is equivalent to

[TABLE]

Hence, $\rho^{\prime}$ and $\sigma^{\prime}$ correspond directly to each other, i.e. $\rho^{\prime}\equiv\mathord{\mathit{chr}}(\sigma^{\prime})$ and therefore rule transitions in the translation are complete w.r.t. the abstract operational semantics of ACT-R. ∎

Theorem 6.5 (soundness and completeness of translation).

For an ACT-R model $M$, ACT-R states $\sigma$ and $\sigma^{\prime}$ and their CHR counterparts $\mathord{\mathit{chr}}(M),\mathord{\mathit{chr}}(\sigma)$ and $\mathord{\mathit{chr}}(\sigma^{\prime})$ the following propositions are equivalent:

1. (1)

$\sigma\rightarrowtail\sigma^{\prime}$* in the model $M$* 2. (2)

$\mathord{\mathit{chr}}(\sigma)\mapsto\mathord{\mathit{chr}}(\sigma^{\prime})$**

Proof.

This follows directly from lemmas 6.2, 6.3 and 6.4. ∎

7. Related Work

We want to highlight the contribution of (Albrecht and Westphal, 2014) that we have used as a starting point to improve our work by unifying and extending it by our needs. We discuss this line of work in detail in section 7.1. In section 7.2 we summarize other work related to this paper.

7.1. Formal Semantics According to Albrecht et al.

The formalization according to (Albrecht and Westphal, 2014) has been developed independently from our work in (Gall, 2013; Gall and Frühwirth, 2015a). Our very abstract semantics is based on it. (Albrecht and Westphal, 2014) basically defines a general production rule system that works on sets of buffers and chunks without specifying actual matching, actions and effects for the sake of modularity and reusability. We briefly summarize the differences between the semantics in (Albrecht and Westphal, 2014) and our very abstract semantics. For details, we refer to the original papers. The nomenclature in this paper differs in some points from the original paper (Albrecht and Westphal, 2014) to unify it with our previous work. We omit module queries for the sake of brevity.

The sets of buffers $\mathbb{B}$ and action symbols $A$ are defined as in section 2. For the sake of brevity, we have omitted the so-called buffer queries in our definition of the very abstract semantics. Queries are an additional type of test on the left-hand side of a rule. The very abstract semantics can be easily extended by queries. We have adopted the definition of chunk types, chunks and cognitive states from the formalization of (Albrecht and Westphal, 2014), although the set of chunks in (Albrecht and Westphal, 2014) should be a multi-set as example 3.3 shows. However, we have reduced the definition in our very abstract semantics by omitting the notion of a finite trace, which is a sequence $\gamma_{0},\gamma_{1},\dots\in\Gamma^{*}$ of cognitive states. Those traces are used to compute the effects of an action. This definition seems inaccurate as the information of a finite trace that only logs the contents of the buffers at each step does not suffice to calculate sub-symbolic information. In typical definitions the calculation of production rule utilities needs the times of all rule applications that are not part of the trace. In other implementations and instantiations of ACT-R, there can be more additional information that is needed for sub-symbolic calculations. That is why we have extended the states by a parameter valuation function that abstracts from the information needed and leaves it to the architecture to define which information is stored.

In (Albrecht and Westphal, 2014), effects of actions with action symbol $\alpha\in A$ are defined by an interpretation function $I_{\alpha}:\Pi\rightarrow 2^{\Gamma_{\mathord{\mathrm{part}}}\times 2^{\Delta}}$ (we have omitted queries as stated before). Similarly to the very abstract semantics, it assigns to each finite trace the possible effects of an action. Effects are a partial cognitive state that overwrites the contents of the buffers as in the very abstract semantics and a set $C\subseteq\Delta$ that defines the chunks that are removed. In typical implementations of ACT-R, the chunks in $C$ are moved to the declarative module which explains the need to define such a set. We have generalized this information by the notion parameter valuations that can be manipulated by an interpretation function. This enables us to abstract from the specific concept of moving chunks to declarative memory in our abstract semantics for example. Note that in (Albrecht and Westphal, 2014), the combination of interpretation functions to a rule interpretation is only stated informally. Additionally, we have extended the domain of an action interpretation function to actions, i.e. terms over the actions symbols in $A$, and states instead of only action symbols, since more information is needed to calculate, like the parameters of the actions (i.e. the slot-value pairs) and information from the state.

The production rule selection function $S:\Pi\rightarrow 2^{\Sigma}$ maps a set of applicable rules to each finite trace. In the very abstract semantics we have extended the domain from traces to a whole state since again additional information might be needed to resolve rule conflicts. With parameter valuations, we abstract from the information that is actually needed and leave it to the architecture definition. Additionally, our definition of selection function adds the notion of variable bindings that are not considered in (Albrecht and Westphal, 2014).

The operational semantics in (Albrecht and Westphal, 2014) is defined as a labeled, timed transition system with the following transition relation $\rightsquigarrow$ over time-stamped cognitive states from $\Gamma\times\mathbb{R}_{0}^{+}$:

[TABLE]

for a production rule $r\in\Sigma$, an execution delay $d\in\mathbb{R}^{+}_{0}$, a set of chunks $\omega\subseteq\Delta$ and a finite trace $\pi\in\Pi$, if and only if $r\in S(\pi,\gamma)$, i.e. $r$ is applicable in $\gamma$, the actions of $r$ according to the interpretation functions yield $\gamma^{\prime}$ and $t^{\prime}=t+d$.

Note that the set of chunks $\omega$ has been used but never defined in the original paper (Albrecht and Westphal, 2014). We suspect that it represents an equivalent to the chunk store from our abstract semantics, i.e. the used subset of all possible chunks (which is how $\Delta$ is defined according to the paper). Although we consider it an integral part of ACT-R, the matching of rules – and particularly binding of variables by the matching – is completely hidden in $S$ or even not defined. On the one hand this simplifies exchanging the matching, on the other hand the function $S$ should then be defined slightly different to enable proper handling of variable bindings and conflict resolution as we discuss in section 3.

In the original semantics according to (Albrecht and Westphal, 2014) there is no definition of what happens if there is no rule applicable, but there are still effects of e.g. requests that can be applied. We have treated this case by adding the no rule transition to the very abstract semantics.

7.2. Other Work

The reference implementation of ACT-R is described in a technical document (Bothell, ) that defines the operational semantics mostly verbally and determines various technical details that are important for this exact implementation but not the architecture itself. In (Gall and Frühwirth, 2015), we have defined a semantics that describes the core of the reference implementation of ACT-R and show that every transition possible in this refined semantics is also possible in the abstract semantics. This shows that formal reasoning about our abstract semantics is meaningful to actual implementations.

There are approaches of implementing ACT-R in other languages, for example a Python implementation (Stewart and West, 2007) or (at least) two Java implementations (Harrison, 2008; Salvucci, ). All those approaches do not concentrate on formalization and analysis, but only introduce new implementations. In (Stewart and West, 2007) it is stated that exchanging integral parts of the ACT-R reference implementation is difficult due to the need of an extensive knowledge of technical details. They propose an architecture that is more concise and reduced to the fundamental concepts (that they also identify in their paper). However, their work still lacks a formalization of the operational semantics.

In (Albrecht et al., 2014), the authors summarize the work on semantics in the ACT-R context. They also come to the conclusion that there are only new implementations available that sometimes try to formalize parts of the architecture, but no formal definition of ACT-R’s operational semantics. The authors use this result as a motivation for their work in (Albrecht and Westphal, 2014).

We describe an adaptable implementation of ACT-R using Constraint Handling Rules (CHR) in (Gall, 2013; Gall and Frühwirth, 2014, 2015b) that is based on our formalization. Due to the declarativity of CHR, the implementation is very close to the formalization and easy to extend. This has been proved by exchanging the conflict resolution mechanism (that is an integral part of typical implementations) with very low effort (Gall and Frühwirth, 2014). Even the integration of refraction, i.e. inhibiting rules to fire twice on the same (partial) state, has been exemplified and can be combined with other conflict resolution strategies. The translation presented there is close to both the core of the reference implementation and the abstract semantics whose abstract parts are defined such that the match the reference implementation and some of its extensions.

8. Conclusion

In this paper, we have defined a very abstract operational semantics for ACT-R that can serve as a common base to analyze other operational semantics since it leaves enough room for various ACT-R variants. We then have refined this semantics to an abstract semantics.

Similar to the very abstract semantics, the abstract semantics abstracts from details like timings, latencies, forgetting, learning and specific conflict resolution. However, it defines the matching of rules and the processing of actions as they are typically found in ACT-R implementations. Hence, the abstract semantics concentrates on an abstract version of the typical implementations of ACT-R’s procedural system. This makes it possible to reason about the general transitions that are possible in many ACT-R implementations.

We have defined a translation of ACT-R models to Constraint Handling Rules (CHR) that is sound and complete w.r.t. our abstract semantics of ACT-R. To the best of our knowledge, the abstract semantics together with the sound and complete translation to CHR is the first formal formulation of ACT-R that is suitable to implementation.

For the future, we want to investigate how we can use our abstract semantics in practice, since the faithful embedding in CHR opens many possibilities to reason about cognitive models by applying theoretical results from the CHR world to ACT-R models. For instance, confluence is the property that a program always yields the same result for the same input regardless of the order rules are applied. In CHR, there is a decidable confluence criterion for terminating programs (Frühwirth, 2009). Although the human mind is probably not confluent because there are many competing strategies with different outputs for the same task, there are always sequences of rules in cognitive models that should not be interfered by any other rule. A confluence criterion helps identifying the parts of the model that are not confluent. This can improve model quality by allowing for controlled non-confluence where desired guaranteeing the rules in the rest of the program not interfering with each other.

However, in practice confluence usually is too strict. With the notion of invariant-based confluence (Duck et al., 2007) only valid states that can be reached are considered, making confluence analysis applicable for practical use. Confluence modulo equivalence (Christiansen and Kirkeby, 2016) is a recent approach to test if programs always yield states that are considered equivalent by an arbitrary definition of state equivalence for the same input. This could be used to analyze if an ACT-R model always yields a certain class of chunks for the same input. For instance it could be interesting for the modeler to know if a certain buffer always contains a chunk of a certain chunk type or with a certain value in some slot at the end of a computation. By that method, models could guarantee certain properties on their final states improving explanatory power and quality of cognitive models.

To make predictions on the probability that a cognitive model has a certain result, we plan to use the CHR extension CHRiSM (Sneyers et al., 2010; Sneyers et al., 2009) that allows to enrich CHR rules with probabilities. It supports probability computation and even an expectation-maximization learning algorithm that could be used for parameter learning of cognitive models.