ρLog

A system for rule-based programming in Mathematica

ρLog is a system for rule-based programming with reduction strategies. It is implemented in the Wolfram Language as an add-on package that extends the rule-based programming capabilities of Mathematica in significant ways. Its theoretical foundation is a calculus for rule-based programming designed by us in 2004, which was called ρLog too.

The ρLog calculus was also used to implement PρLog, an experimental tool that extends logic programming with strategic conditional transformation rules. PρLog combines Prolog with the ρLog calculus.

Rule-based programming with reduction strategies is a programming style similar to logic programming: Programs consists of general clauses of the form

${\displaystyle H/;L_1\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->L_n}$

• the head H of the clause is a reducibility atom of the form
  • ${\displaystyle stg\because <!--\; \because \; -->s}$ with the intended reading "s holds according to strategy stg", or
  • ${\displaystyle s{\to <!--\; \to \; -->}_{stg}t}$ with the intended reading "s is reducible to t with strategy stg".
  • stg is of the form sId or sId[ts], where
    • sId is a string called the identifier of stg, and
    • ts can be any term sequence.
  • the body of the clause is a conjunction of literals L₁,...,L_n. A literal is an atom or the negation of an atom, where atom is either (1) a reducibility atom ${\displaystyle stg\because <!--\; \because \; -->s}$ or ${\displaystyle s{\to <!--\; \to \; -->}_{stg}t}$, or (2) any boolean expression of Mathematica, that is, an expression that Mathematica evaluates to True or False
    When n=0, the body is empty and we write the clause in the form H.
  Like in Logic Programming, the intended reading of this program clause is "$H$ holds if $L_1$ and ... and $L_{\mathrm{n}}$ hold." The literals $L_1$, ..., $L_{\mathrm{n}}$ form the body of the program clause.

  We call these kinds of program clauses strategic conditional transformation rules because they can have reducibility atoms which strategies that specify how to check their satisfiability.

  There are some important similarities and differences between Prolog and ρLog:
  1. Prolog is for Logic Programming, where program clauses are of the form
     ${\displaystyle p(t_1,\dots <!--\; \dots \; -->,t_m)\leftarrow <!--\; \leftarrow \; -->L_1\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->L_n.}$
     Such a clause provides a partial definition for the predicate whose name is p.
     ρLog is for Rule-based Programming, where program clauses do not define predicates but strategies: A program clause
     ${\displaystyle s{\to <!--\; \to \; -->}_{stg}t/;L_1\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->L_n}$
     provides a partial definition which is associated with the identifier of strategy stg.
  2. In Prolog, objects are denoted by ordinary terms t from first-order logic (FOL) defined by the grammar
     ${\displaystyle t::=X|f(t_1,\dots <!--\; \dots \; -->,t_n)}$
     where X is an ordinary variable and f is a function symbol of rank n.
     In ρLog, objects are denoted by terms from a language which extends the language of FOL with more kinds of variables: ordinary variables x,y,z,...(for terms), function variables F,G,... (for function symbols), sequence variables X,Y,Z,... (for finite sequences of terms), and context variables F^o,G^o,H^o,... (for terms with one hole). Terms t and term sequences ts are defined by mutual recursion as follows:
     t ::= x | f[ts] | F[ts] | C^o[t]
     ts ::= t | X | ()
     where () denotes the empty sequence of terms. Ordinary variables, function variables, and sequence variables are characteristic to the Mathematica language, whereas context variables are a novelty of ρLog. Therefore, in ρLog we can write very concise and easy-to-understand program specifications, which are cumbersome or impossible to express in Prolog.
  3. In Prolog we rely on mgu-based SLDNF-resolution to answer queries, but in ρLog we can not because the unification problem of ρLog terms is not finitary. For example, the terms f(a,X) and f(X,a) have infinitely many most general unifiers: ${\displaystyle \{X\to <!--\; \to \; -->()\},\{X\to <!--\; \to \; -->(a)\},\{X\to <!--\; \to \; -->(a,a)\}}$, etc.
     The good news is that matching in ρLog is finitary. Therefore, we impose a natural syntactic restriction on programs and queries called determinism, which guarantees that we can rely on matching-based SLDNF-resolution to answer queries.

  Determinism

  ρLog is designed to check the satisfiability of queries with respect to a given program. A query is a logical conjunction of literals ${\displaystyle L_1\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->L_n}$ where all variables are existentially quantified by default. ρLog is designed to answer queries Q, that is, to find substitutions θ such that Qθ can be deduced from the definitions of strategy combinators and strategies defined so far. Like Prolog, ρLog computes so-called answer substitutions using a form of SLDNF-resolution which is adapted for rule-based programming with reduction strategies. The literals of the goal are answered from left to right.

  To ensure that queries can be answered by matching instead of unification we impose a very natural syntactic restriction on queries and program clauses, called determinism:

  • if W is a set of variables, we say that a query Q=L₁∧...∧L_i∧...∧L_n is W-deterministic if the following condition is satisfied for every ${\displaystyle 1\le <!--\; \le \; -->i\le <!--\; \le \; -->n}$:
    • If L_i is ${\displaystyle s{\to <!--\; \to \; -->}_{stg}t}$ or ${\displaystyle stg\because <!--\; \because \; -->s}$ or Not[${\displaystyle stg\because <!--\; \because \; -->s}$] or Not[expr] where expr is a boolean expression of Mathematica, then ${\displaystyle Vars(stg,s)\subseteq <!--\; \subseteq \; -->W\cup <!--\; \cup \; -->\underset{j=1}{\overset{i-<!--\; -\; -->1}{\bigcup <!--\; \bigcup \; -->}}Vars(L_j)}$
    • If L_i is Not[${\displaystyle s{\to <!--\; \to \; -->}_{stg}t}$] then ${\displaystyle Vars(stg,s)\subseteq <!--\; \subseteq \; -->W\cup <!--\; \cup \; -->\underset{j=1}{\overset{i-<!--\; -\; -->1}{\bigcup <!--\; \bigcup \; -->}}Vars(L_j)}$ and ${\displaystyle \left(Vars(t)-<!--\; -\; -->\left(W\cup <!--\; \cup \; -->\underset{j=1}{\overset{i-<!--\; -\; -->1}{\bigcup <!--\; \bigcup \; -->}}Vars(L_j)\right)\right)\cap <!--\; \cap \; -->\underset{j=i+1}{\overset{n}{\bigcup <!--\; \bigcup \; -->}}Vars(L_j)=\mathrm{\varnothing <!--\; \varnothing \; -->}}$
  • A query is deterministic if it is ∅-deterministic.
  • A program clause ${\displaystyle stg\because <!--\; \because \; -->s/;Q}$ is deterministic if Q is a Vars(s,stg)-deterministic query.
  • A program clause ${\displaystyle s{\to <!--\; \to \; -->}_{stg}t/;Q}$ is deterministic if ${\displaystyle Vars(t)\subseteq <!--\; \subseteq \; -->vars(stg,s)\cup <!--\; \cup \; -->Vars(Q).}$ and Q is a Vars(s,stg)-deterministic query.

  Examples. The following program clauses are deterministic and define strategy "qsort" to sort a list of numbers by quicksort:

  ${\displaystyle \{\}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{qsort}\mathtt{"}}\{\}}$
  ${\displaystyle xs\mathrm{\_<!--\; \_\; -->}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{qsort}\mathtt{"}}\mathtt{Join}[as,bs]/;(xs{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{split}\mathtt{"}}\{l1\mathrm{\_<!--\; \_\; -->},l2\mathrm{\_<!--\; \_\; -->}\})\wedge <!--\; \wedge \; -->}$
  ${\displaystyle (l1{\to <!--\; \to \; -->}_{\mathtt{"qsort"}}as\mathrm{\_<!--\; \_\; -->})\wedge <!--\; \wedge \; -->(l2{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{qsort}\mathtt{"}}bs\mathrm{\_<!--\; \_\; -->})\{x\mathrm{\_<!--\; \_\; -->}\}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{split}\mathtt{"}}\{\{\},\{x\}\}}$
  $\{x\mathrm{\_<!--\; \_\; -->},y\mathrm{\_<!--\; \_\; -->},ys\mathrm{\_<!--\; \_\; -->}\mathrm{\_<!--\; \_\; -->}\mathrm{\_<!--\; \_\; -->}\}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{split}\mathtt{"}}\{as,\mathtt{Prepend}[bs,y]\}/;(x\le <!--\; \le \; -->y)\wedge <!--\; \wedge \; -->$
  $(\{x,ys\}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{split}\mathtt{"}}\{as\mathrm{\_<!--\; \_\; -->},bs\mathrm{\_<!--\; \_\; -->}\})$
  $\{x\mathrm{\_<!--\; \_\; -->},y\mathrm{\_<!--\; \_\; -->},ys\mathrm{\_<!--\; \_\; -->}\mathrm{\_<!--\; \_\; -->}\mathrm{\_<!--\; \_\; -->}\}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{split}\mathtt{"}}\{\mathtt{Prepend}[as,y],bs\}/;(x>y)\wedge <!--\; \wedge \; -->$
  $(\{x,ys\}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{split}\mathtt{"}}\{as\mathrm{\_<!--\; \_\; -->},bs\mathrm{\_<!--\; \_\; -->}\})$
  
  and ${\displaystyle \{\mathtt{4}\mathtt{,}\mathtt{1}\mathtt{,}\mathtt{5}\mathtt{,}\mathtt{2}\}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{q}\mathtt{s}\mathtt{o}\mathtt{r}\mathtt{t}\mathtt{"}}x\mathrm{\_<!--\; \_\; -->}}$ is a deterministic query which asks for the value of the ordinary variable x to which the list {4,1,5,2} gets reduced with strategy "qsort". The expected answer is ${\displaystyle \{x\to <!--\; \to \; -->\{\mathtt{1}\mathtt{,}\mathtt{2}\mathtt{,}\mathtt{4}\mathtt{,}\mathtt{5}\}\}}$.

  The strategy "rw"[s] defined below is for term rewriting with an arbitrary strategy s:

  ${\displaystyle C{\mathrm{\_<!--\; \_\; -->}}^{\mathtt{o}}[x\mathrm{\_<!--\; \_\; -->}]{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{r}\mathtt{w}\mathtt{"}[s\mathrm{\_<!--\; \_\; -->}]}{C}^{\mathtt{o}}[y]/;(x{\to <!--\; \to \; -->}_{s}y\mathrm{\_<!--\; \_\; -->})}$
  
  Remarks:
  1. The strategy "qsort" is defined by two program clauses: one for sorting the empty list, and another for sorting a nonempty list.
  2. "qsort" depends on the auxiliary strategy "split" which splits a nonempty list into two lists: the list of elements smaller than the first element, and the list of elements smaller or equal to the first element, including the first element itself.
  3. We can use of the predefined operations of Mathematica. In this example we use Join to join lists, and Prepend to add an element in front of a list.
  4. We use the syntax of Mathematica to recognize the different kinds of variables:
     • The ordinary variables and the function variables correspond to the occurrences of symbols whose first occurrences are followed by one underscore character '_'. In our example, x,y,l1,l2,xs,as,bs are ordinary variables.
     • The sequence variables correspond to the occurrences of symbols whose first occurrences are followed by three underscore characters , that is, by '___'. In our example, ys is a sequence variable.
     • The context variables correspond to occurrences of expressions of the form C^o or C_^o where C is a Mathematica symbol. Only the occurrences in the first term of the name C of the context variable should be in an expression C_^o;

  Strategies

  Strategies are the core concept of rule-based programming. Every reducibility atom ${\displaystyle stg\because <!--\; \because \; -->s}$ or ${\displaystyle s{\to <!--\; \to \; -->}_{stg}t}$ has a component stg which controls how to check that the atom is satisfiable. The satisfiability test of a deterministic query ${\displaystyle L\wedge <!--\; \wedge \; -->Q}$ always starts from L. A successful satisfiability test of L yields a computed answer θ which instantiates all variables in L with ground terms, and the computation continues by checking the satisfiability of the deterministic query Qθ. Thus, the satisfiability test of a deterministic query ${\displaystyle Q=L_1\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->L_n}$ is performed by computing the derivations
  ${\displaystyle Q=L_1\wedge <!--\; \wedge \; -->L_2\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->L_n{\Rightarrow <!--\; \Rightarrow \; -->}_{{\mathrm{\theta <!--\; \theta \; -->}}_1}(L_2\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->L_n){\mathrm{\theta <!--\; \theta \; -->}}_1{\Rightarrow <!--\; \Rightarrow \; -->}_{{\mathrm{\theta <!--\; \theta \; -->}}_2}\dots <!--\; \dots \; -->{\Rightarrow <!--\; \Rightarrow \; -->}_{{\mathrm{\theta <!--\; \theta \; -->}}_n}\mathrm{◻<!--\; ◻\; -->}}$, abbreviated ${\displaystyle Q{\Rightarrow <!--\; \Rightarrow \; -->}_{\mathrm{\theta <!--\; \theta \; -->}}^{\ast <!--\; \ast \; -->}\mathrm{◻<!--\; ◻\; -->}}$
  where ${\displaystyle \mathrm{\theta <!--\; \theta \; -->}={\mathrm{\theta <!--\; \theta \; -->}}_1{\mathrm{\theta <!--\; \theta \; -->}}_2\dots <!--\; \dots \; -->{\mathrm{\theta <!--\; \theta \; -->}}_n}$ is the answer for Q computed by this derivation.

  For programming purposes, the user must only know the meanings of the deterministic queries ${\displaystyle s{\to <!--\; \to \; -->}_{stg}t}$ and ${\displaystyle stg\because <!--\; \because \; -->s}$ by looking at the syntactic structure of stg. Note that determinism implies that the expressions stg and s are ground.

  In ρLog, strategies are defined by the following grammar:
  ${\displaystyle \begin{array}{rl}stg::=& sId\\ \mid <!--\; \mid \; -->& sId[ts]\\ \mid <!--\; \mid \; -->& st{g}_1\circ <!--\; \circ \; -->st{g}_2\\ \mid <!--\; \mid \; -->& st{g}_1|\dots <!--\; \dots \; -->|st{g}_n\\ \mid <!--\; \mid \; -->& st{g}^{\ast <!--\; \ast \; -->}\\ \mid <!--\; \mid \; -->& \mathtt{N}\mathtt{F}[stg]\\ \mid <!--\; \mid \; -->& \mathtt{F}\mathtt{s}\mathtt{t}[st{g}_1,\dots <!--\; \dots \; -->,st{g}_n]\\ \mid <!--\; \mid \; -->& \mathtt{C}\mathtt{U}\mathtt{T}[stg]\end{array}}$
  where sId is a strategy name (a Mathematica string), ts is a term sequence.

  Strategies specified by program clauses

  The first two kinds of strategies, stg∈{sId,sId[ts]}, are specified by general program clauses
  ${\displaystyle stg\because <!--\; \because \; -->s/;Q\text{or}s{\to <!--\; \to \; -->}_{stg}t/;Q}$
  which are either predefined or declared by the user during a ρLog session.

  The following strategies are predefined:

  • "Id" is the strategy for identity:
    ${\displaystyle gt{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{I}\mathtt{d}\mathtt{"}}t}$ is satisfied by any substitution θ which is a matcher of t with gt, that is, tθ=gt. In ρLog we can write ${\displaystyle gt\equiv <!--\; \equiv \; -->t}$ instead of ${\displaystyle gt{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{I}\mathtt{d}\mathtt{"}}t}$.
  • "rw"[stg] is the strategy for term rewriting:
    ${\displaystyle gt{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{r}\mathtt{w}\mathtt{"}[stg]}t}$ is satisfied by any substitution θ for which there is a subterm gt|_p of gt which satisfies ${\displaystyle gt{|}_p{\to <!--\; \to \; -->}_{stg}u}$ and tθ=gt[uθ]_p.
  • "elem" is the strategy for list membership:
    ${\displaystyle gt{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{e}\mathtt{l}\mathtt{e}\mathtt{m}\mathtt{"}}t}$ is satisfied by any substitution θ for which tθ is an element of list gt.

  Strategy combinators

  • "${\displaystyle \circ }$" is the combinator for strategy composition:
    ${\displaystyle gt{\to <!--\; \to \; -->}_{st{g}_1\circ <!--\; \circ \; -->st{g}_2}t}$ is satisfied by any substitution θ for which there is a ground term s such that θ satisfies both ${\displaystyle gt{\to <!--\; \to \; -->}_{st{g}_1}s}$ and ${\displaystyle s{\to <!--\; \to \; -->}_{st{g}_2}t}$.
  • "|" is the combinator for nondeterministic choice:
    ${\displaystyle gt{\to <!--\; \to \; -->}_{st{g}_1|...|st{g}_n}t}$ is satisfied by any substitution θ which satisfies a query ${\displaystyle gt{\to <!--\; \to \; -->}_{st{g}_i}t}$ for some ${\displaystyle 1\le <!--\; \le \; -->i\le <!--\; \le \; -->n}$.
  • "^*" is the combinator for repetition:
    ${\displaystyle gt{\to <!--\; \to \; -->}_{st{g}^{\ast <!--\; \ast \; -->}}t}$ is satisfied by any substitution θ which satisfies ${\displaystyle gt\equiv <!--\; \equiv \; -->t}$ or a query ${\displaystyle (gt{\to <!--\; \to \; -->}_{stg}{s}_1)\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->(s_n{\to <!--\; \to \; -->}_{stg}t)}$ for a finite number of ground terms s₁,...,s_n.
  • "NF" is the normalization combinator:
    ${\displaystyle gt{\to <!--\; \to \; -->}_{\mathtt{N}\mathtt{F}[stg]}t}$ is satisfied by any substitution θ which satisfies ${\displaystyle gt{\to <!--\; \to \; -->}_{st{g}^{\ast <!--\; \ast \; -->}}t}$ and t is irreducible with stg, that is, there is no term u such that ${\displaystyle t{\to <!--\; \to \; -->}_{stg}u}$ is satisfiable.
  • "Fst" is the strategy combinator which behaves as follows:
    ${\displaystyle gt{\to <!--\; \to \; -->}_{\mathtt{F}\mathtt{s}\mathtt{t}[st{g}_1,...,st{g}_n]}t}$ is satisfied by any substitution θ which satisfies ${\displaystyle gt{\to <!--\; \to \; -->}_{st{g}_i}t}$ and i is the smallest index for which gt is reducible with strategy stg_i.
  • "CUT" is a combinator for don't care choice of a reduction:
    • ${\displaystyle gt{\to <!--\; \to \; -->}_{\mathtt{C}\mathtt{U}\mathtt{T}[stg]}t}$ is satisfied by only one substitution θ (don't care which) which satisfies the query ${\displaystyle gt{\to <!--\; \to \; -->}_{stg}t}$
    • ${\displaystyle \mathtt{C}\mathtt{U}\mathtt{T}[stg]\because <!--\; \because \; -->gt}$ is satisfied by only one substitution θ (don't care which) which satisfies the query ${\displaystyle stg\because <!--\; \because \; -->gt}$

  It allows to use arbitrary Mathematica expressions to express conditions in requests and rules. The implementation of our strategy language is based on a revised version of the ρLog calculus.

  The ρLog calculus was also used to implement PρLog, an experimental tool that extends logic programming with strategic conditional transformation rules. PρLog combines Prolog with the ρLog calculus.

  To the top

  User guide

  ρLog is an Add-on package for Mathematica which can be downloaded for free from here. The download is the file RhoLog.wl which should be copied in $UserBaseDirectory/Applications.

  To use ρLog , you should first load it with the command

  <<RhoLog`

  ρLog commands

  DeclareRules[rule₁,...,rule_n]
  adds rule₁,...,rule_n to the set of rules of the current program.
  Rules[sId]
  returns the list of rules specified so far for the strategy with identifier sId. For example,
  Rules["rw"]
  returns the list ${\displaystyle \{x\mathrm{\_<!--\; \_\; -->}{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{r}\mathtt{w}\mathtt{"}\mathtt{[}\mathrm{\rho <!--\; \rho \; -->}\mathtt{\_<!--\; \_\; -->}\mathtt{]}}y/;(x{\to <!--\; \to \; -->}_{\mathrm{\rho <!--\; \rho \; -->}|\mathtt{"}\mathtt{r}\mathtt{w}\mathtt{1}\mathtt{"}[\mathtt{"}\mathtt{r}\mathtt{w}\mathtt{"}[\mathrm{\rho <!--\; \rho \; -->}]]}y\mathrm{\_<!--\; \_\; -->})\}}$, and
  Rules["rw1"]
  returns the list ${\displaystyle \{f\mathrm{\_<!--\; \_\; -->}[as\mathrm{\_<!--\; \_\; -->}\mathrm{\_<!--\; \_\; -->}\mathrm{\_<!--\; \_\; -->},x\mathrm{\_<!--\; \_\; -->},bs\mathrm{\_<!--\; \_\; -->}\mathrm{\_<!--\; \_\; -->}\mathrm{\_<!--\; \_\; -->}]{\to <!--\; \to \; -->}_{\mathtt{"}\mathtt{r}\mathtt{w}\mathtt{1}\mathtt{"}\mathtt{[}\mathrm{\rho <!--\; \rho \; -->}\mathtt{\_<!--\; \_\; -->}\mathtt{]}}f[as,y,bs]/;(x{\to <!--\; \to \; -->}_{\mathrm{\rho <!--\; \rho \; -->}}y\mathrm{\_<!--\; \_\; -->})\}}$.
  Request[Q,options]
  RequestAll[Q,options]
  instruct the system to compute one (resp. all) answer(s) to the query Q with respect to the current program. If the query is unsatisfiable, then Request returns "No solution found.", and RequestAll returns the empty list {}.
  Options:
  • Trace → True|False. If True, it instructs the system to enable tracing, that is, to generate a notebook with a trace of the search for a solution.
  • Depth → nnn imposes the limit nnn on the maximum number of transformation steps in the depth search of a solution for query.
  • MaxSols → nnn is an option for RequestAll. It imposes the limit nnn on the maximum number of solutions for query.
  • ProofSimplify → True|False. If True, it instructs the system to simplify the proof produced by the trace of the computation.
  For example,
  Request[f[g[a,b],g[a,c]]≡F_[C_^o[x_],C^o[y_]]]
  returns the computed answer {"C"→Identity,"F"→f,"x"→g[a,b],"y"→g[a,c]}, and
  Request[f[g[a,b],g[a,c]]≡F_[C_^o[x_],C^o[y_]]]
  returns the list of computed answers {{"C"→Identity,"F"→f,"x"→g[a,b],"y"→g[a,c]]},{"C"→(g[a,#1]&),"F"→f,"x"→b,"y"→c}}.
  Note that, in Mathematica, Identity is the identity function, and (g[a,#1]&) is the function that maps every term t to the term g[a,t]
  ApplyRule[stg,gt,options]
  instructs the system to compute one (if any) reduct of the ground term $\mathrm{gt}$ with strategy stg. ρLog reports "No solution found." if there is no reduct of gt with strategy stg.
  Options:
  • Trace, Depth, and ProofSimplify, with same meaning as for Request.
  ApplyRuleList[stg,gt,options]

  instructs the system to compute all reducts of gt with respect to strategy stg, that is, the list of all ground terms t such that formula $\mathrm{gt}{\to }_{s}t$ holds.

  Options:
  • Trace, Depth, and ProofSimplify, with same meaning as for Request.
  • MaxSols, with the same meaning as for RequestAll.

  To the top

  Running examples

  The Mathematica notebook Examples.nb contains several examples that illustrate rule-based programming techniques in ρLog.

  To the top

  Publications

  The first version of the ρLog calculus is described in

  • Mircea Marin and Temur Kutsia. Foundations of the Rule-Based System ρLog. Journal of Applied Non-Classical Logics, 16(1–2):151–168, 2006. PDF.
  The following papers refer to earlier versions ρLog and indicate some of its applications:
  1. Mircea Marin, Florina Piroi: Deduction and Presentation in ρLog. Electr. Notes Theor. Comput. Sci. 93: 161-182 (2004)
  2. Temur Kutsia, Mircea Marin: Can Context Sequence Matching Be Used for XML Querying? Procs. of UNIF 2005, 77-95 (2005). PDF.
  3. Temur Kutsia, Mircea Marin: Matching with Regular Constraints. LPAR 2005: 215-229 (2005). PDF.
  4. Mircea Marin, Tetsuo Ida: Rule-Based Programming with ρLog. SYNASC 2005: 31-38 (2005). PDF.
  5. Mircea Marin and Temur Kutsia. Foundations of the Rule-Based System ρLog. Journal of Applied Non-Classical Logics, 16(1–2):151–168, 2006. PDF.
  The following papers refer to more recent developments of ρLog:
  1. Mircea Marin, Temur Kutsia, and Besik Dundua: A Rule-based Approach to the Decidability of Safety of ABAC_α. SACMAT 2019:173-178. PDF.
  2. Mircea Marin, Besik Dundua, and Temur Kutsia: A Rule-Based System for Computation and Deduction in Mathematica. WRLA@ETAPS 2020: 57-74. PDF.

  To the top

  Download and installation instructions

  The current distribution is implemented in Wolfram Mathematica 12.3. To install it, do the following steps:

  1. Open Mathematica, and evaluate
     $UserBaseDirectory
     to find out the base directory of your Mathematica installation. Then, close Mathematica.
  2. Download the file RhoLog.wl, and copy it in $UserBaseDirectory/Applications.
  3. Open a Mathematica notebook and load the RhoLog package with the command
     <<RhoLog`
  4. Check if the RhoLog package is available, by evaluating
     ?Request
     If everything worked smoothly, Mathematica will display information about the command Request of RhoLog.

  To the top

  People

  • Mircea Marin
  • Temur Kutsia
  • Besik Dundua