$\rho$Log and RhoLog

$\rho$Log is a calculus designed by us for rule-based programming. RhoLog is a Mathematica package for rule-based programming, based on the $\rho$Log calculus. The current version of RhoLog is implemented in Mathematica 14 and can be downloaded freely from

https://staff.fmi.uvt.ro/~mircea.marin/rholog/RhoLog.wl

$\rho$Log

was designed in 2004 by some members of the Theorema group working on the implementation of an assistant system for doing mathematics by theorem proving and theory exploration, as envisioned by Bruno Buchberger. Its initial purpose was to assist mathematicians to explore theories and search for proofs by letting them specify and execute strategies that combine the capabilities of domain-specific provers, solvers, and computing methods. Our first publications about $\rho$Log [MP04a, MP04b] refer to RhoLog, a Mathematica package based on $\rho$Log, which can be used for computation by deduction, and generation and presentation of proofs in human-readable format. Afterwards, we continued to develop $\rho$Log and the RhoLog package as a standalone system [KM05, MK06, MKD19, MDK20]. A Prolog implementation of $\rho$Log is also available [DKM09].

1 The $\rho$Log calculus

$\rho$Log is a calculus designed for reasoning about the reducibility of terms of the form $\mathrm{𝑠𝑡𝑔}\mathrm{@}s$, which express the application of strategy $stg$ to $s$. We are interested in the reducibility relation $\mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}t$ which is induced by a set $ℛ$ of conditional reduction rules of the form

which we abbreviate by writing . The informal reading of such a rule is “The applicative term $\mathrm{𝑠𝑡𝑔}\mathrm{@}l$ can be reduced to $r$ if conditions $L_1$ and … and $L_n$ hold.” For such a set $ℛ$ we want to find answers to queries

abbreviated , which express a conjunction of logical formulas $L_i$ of four kinds:

1. a constraint over a known constraint domain,

2. a reducibility formula ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{s}_i\to t_i$,

3. The logical negation of ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{s}_i\to t_i$, which we denote by $\mathrm{𝑠𝑡𝑔}\mathrm{@}\nrightarrow t$,

4. A matching formula $s_i\equiv t_i$.

An answer to such a query is a ground substitution $\sigma$ for the variables in the query such that every formula $\sigma (L_i)$ holds in the reduction theory induced by $ℛ$. For our kinds of constraints, this means that: (1) if $L_i$ is a constraint over a known constraint domain then $\sigma (L_i)$ is valid in it; (2) if $L_i$ is $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t$ then $\sigma (\mathrm{𝑠𝑡𝑔}\mathrm{@}s){\to }_{ℛ}\sigma (t)$ holds; (3) if $L_i$ is $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\nrightarrow t$ then $\sigma (\mathrm{𝑠𝑡𝑔}\mathrm{@}s)\to \sigma (r)$ is unsatisfiable, that is, none of the ground instances of $\sigma (\mathrm{𝑠𝑡𝑔}\mathrm{@}s){\to }_{ℛ}\sigma (t)$ holds. By imposing some natural restrictions on the syntactic structure of rules and queries (Section 1.1.3), we can guarantee that $\rho$Log is sound (every computed substitution is an answer to the query) and complete (all awnswers are eventually computed).

$\rho$Log has some outstanding features:

Expressivity:

It’s specification language is in an algebra of terms with four kinds of variables: for terms, for functional symbols, for contexts, and for sequences of terms. As a result, a wide range of applications have natural and concise rule-based specifications.

Performance:

$\rho$Log was designed to be sound and complete in any term algebra where the matching problem is finitary. The term language of $\rho$Log is very well suited from this point of view because:

1. We have shown that the matching problem is finitary, and defined matching calculi in this algebra of terms [KUT04, KUT07].

2. Mathematica [WOL99] is a language with efficient built-in support for rewriting based on matching with variables for terms, function symbols, and sequences of terms. It can be extended easily to perform finitary matching with context variables too. For this reason, we used Mathematica to implement $\rho$Log.

1.1 Syntax

The rule-based programming style proposed by us is concerned with the outcome of applying strategies on objects of interest. The strategies and objects of interest are expressed as terms over a signature $ℱ$ of variadic function symbols, and a set $V=V_i\cup V_f\cup V_c\cup V_s$ of variables of four kinds. The sets $V_i,V_f,V_c,$ and $V_s$ are countably infinite and mutually disjoint. The elements of $V_i$, called individual term variables, have names with superscript $i$, e.g., $x^i,y^i,z^i$; those of $V_f$, called function variables, have names with superscript $f$, e.g., $x^f,y^f,z^f$; those of $V_c$, called context variables, have names with superscript $c$, e.g., $x^c,y^c,z^c$; and those of $V_s$, called sequence variables, have names with superscript $c$, e.g., $x^s,y^s,z^s$. We use $ℱ$ and $V$ to build three kinds of expressions: terms $t\in T(ℱ,V)$, term sequences $ts,t{s}_1,t{s}_2\in TS(ℱ,V)$, and contexts $ctx\in Ctx(ℱ,V)$. They are defined by the grammar

subject to the following restriction: $\bullet \in ℱ$ is a special symbol, called hole, which does not occur in terms or term sequences. The sequence constructor ’,’ is assumed to be associative and with identity element none. Terms and contexts are represented in a simplified form, by removing the occurrences of none and writing $f$ instead of $f()$ whenever $f$ is a function symbol.

Thus, the basic expressions of our language are elements of the syntactic domain

$$Expr(ℱ,V):=T(ℱ,V)\cup ℱ\cup Ctx(ℱ,V)\cup TS(ℱ,V).$$

Notice that a context is like a term, but with exactly one occurrence of the hole. Contexts can be applied to terms or other contexts. If $\mathrm{𝑐𝑡𝑥}$ is a context, and $s$ is a term or context, then the operation $ctx[s]$ of applying $\mathrm{𝑐𝑡𝑥}$ to $s$ is defined as follows:

Strategies

are represented by terms $f(\mathrm{\dots })$ where $f\in ℱ$ is the identifier of a strategy. The distinguished function symbol @ is used to construct terms $\mathrm{@}(\mathrm{𝑠𝑡𝑔},s)$ to indicate the application of strategy $\mathrm{𝑠𝑡𝑔}$ to $s$. We call such terms applicative terms and allow the function symbol @ to occur only at the outermost position of an applicative term. We write $T_{\mathrm{@}}(ℱ,V)$ for the set of applicative terms, $T(ℱ,V)$ for the set of other terms without occurrences of @, and $Vars(e)$ for the set of variables in a syntactic construct $e$. Also, we use $stg\mathrm{@}s$ as an alternative notation for the applicative term $\mathrm{@}(stg,s)$.

1.1.1 Substitutions.

A substitution is a mapping

$$\sigma :V\to T(ℱ,V)\cup ℱ\cup Ctx(ℱ,V)\cup TS(ℱ,V)$$

such that $\sigma (x)\in T(ℱ,V)$ for all $x\in V_i$, $\sigma (F)\in ℱ$ for all $F\in V_f$, $\sigma (C)\in Ctx(ℱ,V)$ for all $C\in V_c$, and $\sigma (\overline{x})\in TS(ℱ,V)$ for all $\overline{x}\in V_s$.

Every substitution $\sigma$ can be extended homomorphically to a mapping

$$\sigma :Expr(ℱ,V)\to Expr(ℱ,V).$$

An expression $\sigma (e)$ is called an instance of the expression $e$.

An important property of the term algebra used in our specifications is finitary matching. This means that, for any two terms $s\in T(ℱ,V)$ and $t\in T(ℱ,\mathrm{\varnothing })$ the set of substitutions

$$\mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}(s\ll t):=\{\sigma \mid \sigma (s)=t\}$$

is finite [KUT04, KUT07].

1.1.2 Reducibility and matching formulas.

A reducibility formula is an expression $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t$ with $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\in T_{\mathrm{@}}(ℱ,V)$ and $t\in T(ℱ,V)$. The informal reading of this formula is “the applicative term $\mathrm{𝑠𝑡𝑔}\mathrm{@}s$ is reducible to $t$”. An irreducibility formula is the logical negation of a reducibility formula $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t$, and is denoted by $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\nrightarrow t$. A matching formula is an expression $s\equiv t$ with $s,t\in T(ℱ,V)$. The informal reading of $s\equiv t$ is “$s$ and $t$ are identical”.

1.1.3 Rules and queries.

Strategies are represented by terms $f(\mathrm{\dots })$ where $f\in ℱ$ is the identifier of a strategy. They are defined by rules of the form

(1)

abbreviated , where every condition $L_i$ is either

1. a term from $T(ℱ,V)$ that expresses a constraint over a known constraint domain, or

2. a reducibility formula ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i\to r_i$, or

3. an irreducibility formula ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i\nrightarrow r_i$, or

4. a matching formula $l_i\equiv r_i$.

The informal reading of (2) is “The reducibility formula $\mathrm{𝑠𝑡𝑔}\mathrm{@}l\to r$ holds if the conditions $L_1$, …, $L_n$ hold.”. Rules can be unconditional, that is, of the form . We write them in the simplified form $\mathrm{𝑠𝑡𝑔}\mathrm{@}l\to r$. Occasionally, we write T for the conjunction of zero conditions. We view (2) as a partial definition for the strategy identified by $\mathrm{𝑠𝑡𝑔}$.

We also consider terms for atomic formulas and strategies to prove their truth by reducing them to a constant true. For such terms $t$ we write $\mathrm{𝑠𝑡𝑔}\mathrm{@}s$ instead of $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to \mathrm{𝚝𝚛𝚞𝚎}$, and may have rules of the form

(2)

A query is of the form

abbreviated , where every $L_i$ can be of the same form as a rule condition. Given a set $V_0$ of variables, we say that the query is $V_0$-admissible if we can define the sets of variables $\{V_i\mid 1\le i\le m\}$ while observing the following restrictions:

• If $L_i$ is an atomic constraint then $Vars(L_i)\subseteq V_{i-1}$ and $V_i:=V_{i-1}$.

• If $L_i$ is ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{s}_i\to t_i$ then $Vars({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{s}_i)\subseteq V_{i-1}$, and $V_i:=V_{i-1}\cup Vars(t_i)$.

• If $L_i$ is ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{s}_i\nrightarrow t_i$ then $Vars({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{s}_i)\subseteq V_{i-1}$ and $V_i:=V_{i-1}$.

• If $L_i$ is $s_i\equiv t_i$ then $Vars(s_i)\subseteq V_{i-1}$ and $V_i:=V_{i-1}\cup Vars(t_i)$.

Notice that $V_0\subseteq V_1\subseteq \mathrm{\dots }\subseteq V_m$. We denote by $QVar{s}_{V_0}(Q)$ the set of variables $V_m$ of a $V_0$-admissible query $Q$ of the form , and say that:

• $Q$ is admissible if $Q$ is $\mathrm{\varnothing }$-admissible.

  In particular, the empty query is admissible. We denote it by $\mathrm{\square }$.

• A rule is admissible if the query is $Vars({\mathrm{𝑠𝑡𝑔}}_0\mathrm{@}l)$-admissible.

1.2 Semantics

A set $ℛ$ of admissible rules induces a reduction relation

$${\to }_{ℛ}\subseteq T_{\mathrm{@}}(ℱ,\mathrm{\varnothing })\times T(ℱ,\mathrm{\varnothing })$$

together with a set of answer substitutions

$$Ans(\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t^{\prime })$$

for every $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\in T(ℱ,\mathrm{\varnothing })$ and $t^{\prime }\in T(ℱ,V)$, such that $\mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}{t}^{\prime }\sigma$ holds whenever $\sigma \in Ans(\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t^{\prime })$. These notions are defined simultaneously as follows:

• $\mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}t$ holds if there exists a rule

  and ground substitutions ${\sigma }_0\in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}({\mathrm{𝑠𝑡𝑔}}_0\mathrm{@}l\ll \mathrm{𝑠𝑡𝑔}\mathrm{@}s),{\sigma }_1,\mathrm{\dots },{\sigma }_n$ such that

  1. For all $1\le i\le n$, if ${\overline{\sigma }}_i$ is the substitution ${\sigma }_{i-1}\circ \mathrm{\dots }\circ {\sigma }_1\circ {\sigma }_0$ then

     1. If $L_i$ is an atomic constraint then ${\sigma }_i=ϵ$ and ${\overline{\sigma }}_i(L_i)$ is valid in its corresponding constraint domain.

     2. If $L_i$ is ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i\to r_i$ then ${\sigma }_i\in Ans({\overline{\sigma }}_i({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i){\to }_{ℛ}{\overline{\sigma }}_i(r_i)$.

     3. If $L_i$ is ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i\nrightarrow r_i$ then ${\sigma }_i=ϵ$ and $Ans({\overline{\sigma }}_i({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i)\to \overline{\sigma }(r_i))=\mathrm{\varnothing }$.

     4. If $L_i$ is $l_i\equiv r_i$ then ${\sigma }_i\in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}({\overline{\sigma }}_i(r_i)\ll {\overline{\sigma }}_i(l_i))$.

  2. $t={\sigma }_n({\overline{\sigma }}_n(r))$.

• $Ans(\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t^{\prime })$ is a subset of $\{\sigma \in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}(t^{\prime }\ll t)\mid \mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}t\}$.

$\rho$Log has two distinguished strategy identifiers: Fst and Cut:

• $Ans(\mathrm{𝙵𝚜𝚝}({\mathrm{𝑠𝑡𝑔}}_1,\mathrm{\dots },st{g}_m)\mathrm{@}s\to t^{\prime })$ is either

  • $\mathrm{\varnothing }$ if $Ans({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}s\to t^{\prime })=\mathrm{\varnothing }$ for all $1\le i\le m$, or

  • $Ans({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}s\to t^{\prime })$ if $Ans({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}s\to t^{\prime })\ne \mathrm{\varnothing }$ and $Ans({\mathrm{𝑠𝑡𝑔}}_j\mathrm{@}s\to t^{\prime })=\mathrm{\varnothing }$ for all .

• $Ans(\mathrm{𝙲𝚞𝚝}(\mathrm{𝑠𝑡𝑔})\mathrm{@}s\to t^{\prime })$ is either $\mathrm{\varnothing }$ if $Ans(\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t^{\prime })=\mathrm{\varnothing }$, or a singleton subset of $Ans(\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t^{\prime })$ if $Ans(\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t^{\prime })\ne \mathrm{\varnothing }$. The choice of the singleton subset of $Ans(\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t^{\prime })$ is don’t care, implementation-dependent.

For any strategy $\mathrm{𝑠𝑡𝑔}$ with identifier different from Fst and Cut, we have

• $Ans(\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to t^{\prime })=\{\sigma \mid \mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}t,\sigma \in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}(t^{\prime }\ll t)\}.$

We say that $s\in T(ℱ,\mathrm{\varnothing })$ is $\mathrm{𝑠𝑡𝑔}$-reducible if $\mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}t$ for some term $t\in T(ℱ,\mathrm{\varnothing })$. Otherwise, we say that $s$ is 3 $\mathrm{𝑠𝑡𝑔}$-redex.

Let $Q$ be an admissible query of the form . An answer substitution of $Q$ in the reduction theory induced by $ℛ$ is a composition of $m$ ground substitutions ${\sigma }_1$, …, ${\sigma }_m$ such that, for all $1\le i\le m$, if ${\sigma }_0=ϵ$ and ${\overline{\sigma }}_i$ is the composition of substitutions ${\sigma }_{i-1}\circ \mathrm{\dots }\circ {\sigma }_1\circ {\sigma }_0$ then

1. If $L_i$ is an atomic constraint then ${\sigma }_i=ϵ$ and ${\overline{\sigma }}_i(L_i)$ is valid in its corresponding constraint domain.

2. If $L_i$ is ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i\to r_i$ then ${\sigma }_i\in Ans({\overline{\sigma }}_i({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i)\to {\overline{\sigma }}_i(r_i))$.

3. If $L_i$ is ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i\nrightarrow r_i$ then ${\sigma }_i=ϵ$ and $Ans({\overline{\sigma }}_i({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}{l}_i)\to \overline{\sigma }(r_i))=\mathrm{\varnothing }$.

4. If $L_i$ is $l_i\equiv r_i$ then ${\sigma }_i\in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}({\overline{\sigma }}_i(r_i)\ll {\overline{\sigma }}_i(l_i))$.

We write $Ans(Q)$ for the set of answer substitutions of an admissible query $Q$.

1.3 Inference rules

The admissibility condition on rules and queries allows us to compute the answers of admissible queries by matching only. The calculus of $\rho$Log makes use of the following rules of inference:

1. 
   if $L$ is a valid atomic constraint in its corresponding constraint domain.

2. 
   if $\sigma \in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}(t\ll s)$.

3. 
   if $Ans({\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}s\to t)\ne \mathrm{\varnothing }$ and $Ans({\mathrm{𝑠𝑡𝑔}}_j\mathrm{@}s\to t)=\mathrm{\varnothing }$ for all .

4. 
   if $Ans(\mathrm{𝙲𝚞𝚝}(\mathrm{𝑠𝑡𝑔})\mathrm{@}s\to t)=\{\sigma \}.$

5. 
   if the identifier of $\mathrm{𝑠𝑡𝑔}$ is neither Fst nor Cut,
   is -renamed apart, and $\sigma \in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}({\mathrm{𝑠𝑡𝑔}}_0\mathrm{@}l\ll \mathrm{𝑠𝑡𝑔}\mathrm{@}s)$.

6. 
   if the identifier of $\mathrm{𝑠𝑡𝑔}$ is neither Fst nor Cut,
   is -renamed apart, and $\sigma \in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}({\mathrm{𝑠𝑡𝑔}}_0\mathrm{@}l\ll \mathrm{𝑠𝑡𝑔}\mathrm{@}s)$.

7. 
   if the atempt to prove the satisfiability of the query $\Leftarrow (s{\to }_{\mathrm{𝑠𝑡𝑔}}t)$ fails finitely.

Every rule of inference is of the form $\frac{G}{G^{\prime }}$.

• Rules 2, 4, 5 and 5’ have as side effect the computation of a substitution $\sigma$, and we depict this fact by writing $G{\rightsquigarrow }_{\sigma }{G}^{\prime }$.

• Rules 1, 3 and 6 check if something happens without producing a substitution as side effect. We depict them by writing $G{\rightsquigarrow }_{ϵ}{G}^{\prime }$ where $ϵ$ denotes for the identity substitution.

A $\rho$Log-derivation of a query $Q$ is a sequence of reduction steps

$$Q{\rightsquigarrow }_{{\sigma }_1}{Q}_1{\rightsquigarrow }_{{\sigma }_2}{Q}_2\rightsquigarrow \mathrm{\dots }{\rightsquigarrow }_{{\sigma }_n}{Q}_n$$

and a $\rho$Log-refutation is a $\rho$Log-derivation which ends with the query $\mathrm{\square }$. We abbreviate a $\rho$Log-refutation by writing $Q{\rightsquigarrow }_{\sigma }^{\ast }\mathrm{\square }$ where $\sigma$ is the restriction of the substitution ${\sigma }_n\circ \mathrm{\dots }\circ {\sigma }_2\circ {\sigma }_1$ to $QVar{s}_{\mathrm{\varnothing }}(Q)$.

As usual for refutation-based calculi, the set of answers computed by $\rho$Log is

$$An{s}_{\rho \text{Log}}(Q):=\{\sigma \mid Q{\rightsquigarrow }_{\sigma }^{\ast }\mathrm{\square }\}.$$

It can be shown that $An{s}_{\rho \text{Log}}(Q)=Ans(Q)$. This means that our calculus is sound and complete.

1.4 Some useful strategies

$x^i{\to }_{\mathrm{𝙸𝚍}}{x}^i$

$x^i{\to }_{\mathrm{𝙲𝚘𝚖𝚙}()}{x}^i$

$x^i{\to }_{\mathrm{𝙽𝙵}(s^i)}{x}^i\Leftarrow (x^i{\nrightarrow }_{s^i}{\mathrm{\_}}^i)$

$x^i{\to }_{\mathrm{𝙾𝚛}(s^i,{\mathrm{\_}}^s)}{y}^i\Leftarrow (x^i{\to }_{s^s}{y}^i)$

$x^i{\to }_{\mathrm{𝙾𝚛}({\mathrm{\_}}^i,s{s}^s)}{y}^i\Leftarrow (x^i{\to }_{\mathrm{𝙾𝚛}(s{s}^s)}{y}^i)$

$x^i{\to }_{\mathrm{𝚁𝚎𝚙𝚎𝚊𝚝}({\mathrm{\_}}^i)}{x}^i$

$x^i{\to }_{\mathrm{𝚁𝚎𝚙𝚎𝚊𝚝}(s^i)}{y}^i\Leftarrow x^i{\to }_{\mathrm{𝙲𝚘𝚖𝚙}(s^i,\mathrm{𝚁𝚎𝚙𝚎𝚊𝚝}(s^i))}{y}^i)$

$x^c[y^i]{\to }_{\mathrm{𝚁𝚠}(s^i)}{x}^c[z^i]\Leftarrow (y^i{\to }_{s^i}{z}^i)$

$g^f(x{s}^s,x^i,y{s}^s){\to }_{\mathrm{𝚁𝚠𝟷}(s^i)}{g}^f(x{s}^s,y^i,y{s}^s)\Leftarrow (x^i{\to }_{s^i}{y}^i)$

$y^i{\to }_{\mathrm{𝙾𝚞𝚝𝚎𝚛}(s^i)}{z}^i\Leftarrow (y^i{\to }_{\mathrm{𝙵𝚜𝚝}(s^i,\mathrm{𝚁𝚠𝟷}(\mathrm{𝙾𝚞𝚝𝚎𝚛}(s^i)))}{z}^i)$

$y^i{\to }_{\mathrm{𝙸𝚗𝚗𝚎𝚛}(s^i)}{z}^i\Leftarrow (y^i{\to }_{\mathrm{𝙵𝚜𝚝}(\mathrm{𝚁𝚠𝟷}(\mathrm{𝙸𝚗𝚗𝚎𝚛}(s^i)),s^i)}{z}^i)$

$x^i{\to }_{\mathrm{𝙻𝚊𝚣𝚢𝙴𝚟𝚊𝚕}(s^i)}{y}^i\Leftarrow (x^i{\to }_{\mathrm{𝙽𝙵}(\mathrm{𝙾𝚞𝚝𝚎𝚛}(s^i))}{y}^i)$

$x^i{\to }_{\mathrm{𝚂𝚝𝚛𝚒𝚌𝚝𝙴𝚟𝚊𝚕}(s^i)}{y}^i\Leftarrow (x^i{\to }_{\mathrm{𝙽𝙵}(\mathrm{𝙸𝚗𝚗𝚎𝚛}(s^i))}{y}^i)$

$g^f(){\to }_{\mathrm{𝙵𝚖𝚊𝚙}({\mathrm{\_}}^i)}{g}^f()$

Like in Prolog, we make use of the anonymous variables ${\mathrm{\_}}^i$, ${\mathrm{\_}}^f$, ${\mathrm{\_}}^c$ and ${\mathrm{\_}}^s$ when we don’t care about their corresponding values.

We let the reader to figure out the meanings of the strategies induced by these reduction rules.

2 The RhoLog package

RhoLog is a Mathematica package for rule-based programming, based on the $\rho$Log calculus. The current implementation is for Mathematica 14.

The package is freely available for download from

https://staff.fmi.uvt.ro/~mircea.marin/rholog/RhoLog.wl

2.1 Installation instructions

1. Download the package RhoLog.wl from

   https://staff.fmi.uvt.ro/~mircea.marin/rholog/RhoLog.wl

   and copy it in the directory

   $UserBaseDirectory/Applications
   

2. Open a Mathematica notebook and load RhoLog with the command

   <<RhoLog‘
   

   Check if the RhoLog package is accessible, by evaluating

   ?Request
   

   If everything worked smoothly, Mathematica will display information about the command Request of RhoLog.

2.2 Specification language

Since RhoLog is a Mathematica package, we use the syntax of Mathematica to write terms. Also, we write

• $s{\to }_{\mathrm{𝑠𝑡𝑔}}t$ instead of $stg\mathrm{@}s\to t$, and $s{\nrightarrow }_{\mathrm{𝑠𝑡𝑔}}t$ instead of $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\nrightarrow t$

• $\mathrm{𝑠𝑡𝑔}\text{::}s$ instead of $\mathrm{𝑠𝑡𝑔}\mathrm{@}s\to \mathrm{𝚝𝚛𝚞𝚎}$.

For strategy identifiers, we use strings delimited by double quotes.

2.3 RhoLog commands

2.3.1 Commands for rule declarations

DeclareRule[$rule$]

declares a single rule $rule$, and

DeclareRules[$rul{e}_1,\mathrm{\dots },rul{e}_n$]

declares rules $rul{e}_1,\mathrm{\dots },rul{e}_n$. For example, the strategies with identifiers , , , , , , , , , , , , , , and are predefined in RhoLog:

$\mathrm{𝙳𝚎𝚌𝚕𝚊𝚛𝚎𝚁𝚞𝚕𝚎𝚜}[$

Notice that

• holds iff $s=t$.

• folds iff $lst$ is a list and $t$ is an element of $lst$.

• "Comp" is for sequential composition of reductions:

  "Comp"$[{\mathrm{𝑠𝑡𝑔}}_1,\mathrm{\dots },{\mathrm{𝑠𝑡𝑔}}_n]\mathrm{@}s{\to }_{ℛ}t$ holds iff there exist ground terms $t_1,\mathrm{\dots },t_n$ such that ${\mathrm{𝑠𝑡𝑔}}_1\mathrm{@}s{\to }_{ℛ}{t}_1$, ${\mathrm{𝑠𝑡𝑔}}_2\mathrm{@}{t}_1{\to }_{ℛ}{t}_2$, …, ${\mathrm{𝑠𝑡𝑔}}_n\mathrm{@}{t}_{n-1}{\to }_{ℛ}{t}_n$ hold and $t_n=t$.

• "Or" is for parallel reduction:

  "Or"$[{\mathrm{𝑠𝑡𝑔}}_1,\mathrm{\dots },{\mathrm{𝑠𝑡𝑔}}_n]\mathrm{@}s{\to }_{ℛ}t$ holds iff ${\mathrm{𝑠𝑡𝑔}}_i\mathrm{@}s{\to }_{ℛ}t$ holds for some $1\le i\le n$.

• holds if there exist terms $t_1,\mathrm{\dots },t_n$ in $T(ℱ,\mathrm{\varnothing })$ such that the relations $\mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}{t}_1$, $\mathrm{𝑠𝑡𝑔}\mathrm{@}{t}_1{\to }_{ℛ}{t}_2$, …, $\mathrm{𝑠𝑡𝑔}\mathrm{@}{t}_{n-1}{\to }_{ℛ}{t}_n$ hold, and $t=t_n$. holds if holds for an integer $n\ge 0$.

• "Rw" is for rewriting: holds if (1) $s$ has a subterm $l$ such that $\mathrm{𝑠𝑡𝑔}\mathrm{@}l{\to }_{ℛ}r$, and (2) $t$ is obtained from $s$ by replacing $l$ with $r$.

• "NF" is for normalizing reduction:

  "NF"$[\mathrm{𝑠𝑡𝑔}]\mathrm{@}s{\to }_{ℛ}t$ holds if "Repeat"$[\mathrm{𝑠𝑡𝑔}]\mathrm{@}s{\to }_{ℛ}t$ holds and $\mathrm{𝑠𝑡𝑔}\mathrm{@}t$ is irreducible, that is, there is no $t^{\prime }$ such that $\mathrm{𝑠𝑡𝑔}\mathrm{@}t{\to }_{ℛ}{t}^{\prime }$.

• "Rw1"[$\mathrm{𝑠𝑡𝑔}$] is for reducing a $\mathrm{𝑠𝑡𝑔}$-redex immediately below the root of a term: holds if $s$ is of the form $f[\mathrm{\dots },l,\mathrm{\dots }]$, $t$ is of the form $f[\mathrm{\dots },r,\mathrm{\dots }]$, and $\mathrm{𝑠𝑡𝑔}\mathrm{@}l{\to }_{ℛ}r$ holds.

• "Fmap"$[\mathrm{𝑠𝑡𝑔}]\mathrm{@}s{\to }_{ℛ}t$ holds iff $s$ is a term of the form $f[s_1,\mathrm{\dots },s_n]$, $t$ is of the form $f[t_1,\mathrm{\dots },t_n]$, and $\mathrm{𝑠𝑡𝑔}\mathrm{@}{s}_i{\to }_{ℛ}{t}_i$ hold for all $1\le i\le n$.

• "Outer"$[\mathrm{𝑠𝑡𝑔}]$ is for reducing an outermost $\mathrm{𝑠𝑡𝑔}$-redex, and "Inner" is for reducing an innermost redex.

• "LazyEval"$[\mathrm{𝑠𝑡𝑔}]$ is for lazy evaluation: it normalizes a term by repeated reductions of outermost $\mathrm{𝑠𝑡𝑔}$-redexes.

• "StrictEval"$[\mathrm{𝑠𝑡𝑔}]$ is for strict evaluation: it normalizes a term by repeated reductions of inneermost $\mathrm{𝑠𝑡𝑔}$-redexes.

• "Perm"$\mathrm{@}lst\to t$ holds iff $lst$ is a list and $t$ is a permutation of $lst$.

• "Subset"$\mathrm{@}s\to t$ holds iff $s$ is a set represented by a list and $t$ is a subset of $lst$.

• The defining rules of "Perm" and "Subset" rely on the built-in capabilities of Mathematica for computation and pattern matching:

  • Permutations and Subsets are built-in functions:

    Permutations$[lst]$ returns the list of all distinct permutations of list $lst$;

    Subsets$[s]$ returns the list of all subsets of $s$.

  • $s/;cond$ in Mathematica is a conditional pattern, in the following sense: $\sigma \in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}(s/;cond\ll t)$ iff $\sigma (s)=t$ and $\sigma (cond)$ is true.

  For example, ${𝚜}^{𝚒}/;\mathrm{𝙻𝚒𝚜𝚝𝚀}[𝚜]$ matches a ground term $𝚝$ with matcher $\{{𝚜}^{𝚒}\to 𝚝\}$ if t is a list. Notice the following implementation detail of RhoLog: when used in pattern conditions, the kind superscripts must be removed from the names of variables.

2.3.2 The #1 placeholder.

RhoLog has a special capability: we can use #1 in rules, such that, when we apply the inference rule

with the renamed-apart rule and matcher

$$\sigma \in \mathrm{𝚖𝚊𝚝𝚌𝚑𝚎𝚛𝚜}({\mathrm{𝑠𝑡𝑔}}_0\mathrm{@}l\ll \mathrm{𝑠𝑡𝑔}\mathrm{@}s)$$

then #1 is replaced with $t$ in This capability allows us to specify the behavior of "Fst" as follows:

$\mathrm{𝙳𝚎𝚌𝚕𝚊𝚛𝚎𝚁𝚞𝚕𝚎𝚜}[$

Although the strategies with identifiers "Comp", "NF", "Or", and "Fst" can be defined correctly with the rules mentioned here, this approach would be inefficient. In RhoLog, their implementations are hard-coded.

Rules[ruleId]

returns the list of defining rules for the rule identifier ruleId. For example:

ClearRules[$ruleI{d}_1,\mathrm{\dots },ruleI{d}_n$]

clears the defining rules for the rule identifiers $ruleI{d}_1$, …, $ruleI{d}_n$.

2.3.3 Commands for queries

Request[]

instructs RhoLog to compute one answer substitution of the admissible query For example:

Request[]
{$𝚡\to 𝚊$}

RequestAll[]

instructs RhoLog to compute all answer substitution of the admissible query For example:

RequestAll[]
{$\{𝚡\to \{𝚊,𝚋,𝚋\}\},\{𝚡\to \{𝚋,𝚊,𝚋\}\},\{𝚡\to \{𝚋,𝚋,𝚊\}\}$}

ApplyRule[$\mathrm{𝑠𝑡𝑔},s$]

instructs RhoLog to compute one $t$ such that $\mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}t$ holds.

ApplyRuleList[$\mathrm{𝑠𝑡𝑔},s$]

instructs RhoLog to compute the list of all terms $t$ such that $\mathrm{𝑠𝑡𝑔}\mathrm{@}s{\to }_{ℛ}t$ holds. For example:

ApplyRule["Rw"["elem"],f[{a,{b}}]]
f[a]

ApplyRuleList["Rw"["elem"],f[{a,{b}}]]
{f[a], f[{b}], f[{a,b}]}

The runtime behaviors of the commands for queries can be controlled with the following options:

• Trace -> True | False. If True, a trace of the rule-based computation is generated and shown in a Mathematica nodebook, in human-readable form.

• Depth -> $nnn$ imposes the maximum length limit $nnn$ for $\rho$Log=derivations. This option can force RhoLog to produce so-called pending derivations, which are too short to yield a computed answer.

• MaxSols -> $nnn$ imposes limit $nnn$ on the number of answers to be found. This means that, after finding $nnn$ solutions, RhoLog will stop searching for other answers to the given query.

• ProofSimplify -> True | False enables/disables the simplification of the explanations produced by tracing.

2.4 Examples and applications

Download and check the following examples:

1. ABACSafety.nb: a tool to check the safety of configurations for the attribute-based access control model (ABAC)

2. GraphColoring.nb: graph colorings

3. EquationalReasoning.nb: reasoning in equational theories represented by terminating rewrite systems

4. EvaluationStrategies.nb: evaluation strategies for functional programming

5. PropositionalProver.nb: a rule-based implementation of a propositional prover, based on Genzen’s calculus.