This is important because translators and compilers are based on formal grammars. Solid textbooks on algorithmic lanquages include a chapter or an appendix devoted to formal grammars. Let us consider a formal grammar from the cited Wiki article with the start symbol $S$, the alphabets $N=\{S,\,B \}$ and $\Sigma = \{ a,b,c \}$, and the production rules

  1. $S \rightarrow aBSc$.

  2. $S \rightarrow abc $.

  3. $Ba \rightarrow aB$.

  4. $Bb\rightarrow bb$.

I try to obtain the theorem $S\rightarrow aabbcc$, making use of FindEquationalProof.

I write down the following axioms:

ClearAll["Global`*"]; axioms = {aBSc == pr[S], abc == pr[S], aB == pr[Ba], bb == pr[Bb]}


FindEquationalProof[aabbcc == pr[S], axioms]

results in

Why the Beep? The kernel Local has quit (exited) during the course of an evaluation.

Is there a workaround? My comp is not powerful.

  • $\begingroup$ @Somos: Are you serious? I wrote down axioms as well as the theorem aabbcc == pr[S] as equalities. Thank you anyway. $\endgroup$
    – user64494
    Commented May 15, 2019 at 17:03
  • $\begingroup$ BTW, LL(1) grammars were realized in Pascal as a student work in 90s. The code takes three pages. $\endgroup$
    – user64494
    Commented May 15, 2019 at 17:29
  • 1
    $\begingroup$ s="S"; Do[s=Select[Flatten[Map[StringReplaceList[s,#]&,{"S"->"aBSc", "S"->"abc", "Ba"->"aB", "Bb"->"bb"}]],StringLength[#]<7&]; If[s=={},Break[]]; Print[s]; ,{10}] instantly displays even on a slow computer {aBSc,abc} {aBabcc} {aaBbcc} {aabbcc} Perhaps someone else can show a better or simpler method. The `Select[...StringLength[#]<7&] discards productions of length greater than 6 because none of your grammer produces a shorter string from a longer string and thus longer strings can never succeed. $\endgroup$
    – Bill
    Commented May 15, 2019 at 20:02
  • 1
    $\begingroup$ NestWhileList[SubstitutionSystem[{"S":> RandomChoice[{"aBSc","abc"}],"Ba"-> "aB","Bb"-> "bb"},#]&,"S",!StringMatchQ[#,"aabbcc"]&,1,10] $\endgroup$
    – chuy
    Commented May 15, 2019 at 20:34
  • $\begingroup$ @Bill: Could you present your comment as an answer (of course, giving us more details and commenting it)? TIA. $\endgroup$
    – user64494
    Commented May 16, 2019 at 11:22

3 Answers 3


The documentation for StringReplaceList says it gives a list of the strings obtained by replacing each individual occurrence of substrings. That seems closer to the desired goal than doing all applicable substitutions over the entire string, but I still do not trust this. This also seems preferable to randomly applying productions, which can sometimes generate a string of terminals, jam and thus not find the desired sequence of productions.

StringReplaceList doesn't seem to accept a list of strings and a list of replacements, so I use Map to do the list of replacements on each of the strings generated thus far by the grammar and then Flatten to merge all those generated strings into one list.

As others have mentioned, we need some terminating condition for success, otherwise the number and length of strings grows without bounds. I considered doing a Union on the generated list of strings, which would remove duplicates. I also considered removing any strings which had been previously generated.

Because the particular grammar being investigated cannot reduce the length of any string I chose to eliminate any strings which are longer than the goal string. For this particular grammar that seemed to focus the process on finding the desired goal string.

When all strings generated in a particular step consist of terminals then StringReplaceList will find no substitutions and will return the empty list. I use that as an exit condition.

I wrap all this inside a Do loop because I was concerned about an infinite stream of productions.


      Map[StringReplaceList[s,#]&,{"S"->"aBSc", "S"->"abc", "Ba"->"aB", "Bb"->"bb"}]],

instantly displays even on a slow computer the result of each step of the productions:

 {aBSc,abc} {aBabcc} {aaBbcc} {aabbcc}

I am still not certain that the pattern matching behavior of StringReplaceList exactly matches what we want for any grammar. Perhaps crafting some grammars with the intent of exposing flaws in the pattern matching process might be worthwhile. And perhaps someone else can show a better or simpler method or discover a flaw anywhere in this.

  • 1
    $\begingroup$ There are wishes and there is reality. I accept your answer. $\endgroup$
    – user64494
    Commented May 16, 2019 at 19:15

While the Lispy notation and formalism is syntactically hideous (improvements welcome), the following gets a bit closer to the question by using FindEquationalProof. The cons here is a nod to the Lisp cons function, but here it's done to create a term. This was done in Mathematica 12:

axiom1 = {ForAll[{x}, cons[S, x] == cons[a, cons[B, cons[S, cons[c, x]]]]]}
axiom2 = {ForAll[{x}, cons[S, x] == cons[a, cons[b, cons[c, x]]]]}
axiom3 = {ForAll[{x}, cons[a, cons[B, x]] == cons[B, cons[a, x]]]}
axiom4 = {ForAll[{x}, cons[B, cons[b, x]] == cons[b, cons[b, x]]]}
grammar = Union[axiom1, axiom2, axiom3, axiom4]
FindEquationalProof[cons[S, nil] == cons[a, cons[a, cons[b, cons[b, cons[c, cons[c, nil]]]]]], grammar]
  • $\begingroup$ +1 (I can't vote up several times.). Many thanks from me to you. Your approach is natural since every formal grammar can be treated as a formal (axiomatic) theory. Unfortunately, your code performs TemplateBox[{"SystemProcesses", "cloudf", "\"\:f7c1\:f7c9\:f7c8RowBox[{\"\\:f3b5\", StyleBox[TagBox[\"SystemProcesses\", Function[Short[Slot[1], 5]]], ShowStringCharacters -> False], \" is not currently supported in the Wolfram Cloud.\\:f3b5\"}]\:f7c0\"", 2, 6, 1, 33717716096517867441, "Local"}, "MessageTemplate"] in MathematicaOnline and crashes my weak comp $\endgroup$
    – user64494
    Commented Nov 28, 2019 at 6:00
  • $\begingroup$ @user64494: Since I'm hardly any kind of expert in Mathematica, I can only guess as to the nature of the problem, but it seems like some extraneous, perhaps invisible, characters crept in to the Mathematica online code. Try typing the whole first line (axiom1 = {ForAll[{x}, cons[S, x] == cons[a, cons[B, cons[S, cons[c, x]]]]]}) into Mathematica online by hand, character by character, and see if the problem comes up again. $\endgroup$
    – ShyPerson
    Commented Dec 1, 2019 at 3:04
  • $\begingroup$ In fact, it works: ProofObject is produced. Thank you again. $\endgroup$
    – user64494
    Commented Dec 15, 2019 at 13:19
  • $\begingroup$ @user64494: Great! Glad to hear it. $\endgroup$
    – ShyPerson
    Commented Dec 16, 2019 at 5:39

Interesting question. This isn't a full answer.

r1 = "S" -> "aBSc";
r2 = "S" -> "abc";
r3 = "Ba" -> "aB";
r4 = "Bb" -> "bb";
rules = {r1, r2, r3, r4};

Now brute force Monte Carlo our way to an answer to how to derive your string. Bunch of problems here, as for example if it is not derivable the loop will run until the Earth cools, it applies the rule to the first match always, etc.

init = "S";
While[init != "aabbcc",
        transforms = {};
        res = FixedPointList[
                   StringReplace[#, (r = RandomChoice[rules]; transforms = {transforms, r}; r), 1] &, 
        init = res // Last
transforms // Flatten//Most

{"S", "aBSc", "aBabcc", "aaBbcc", "aabbcc"}

{"S" -> "aBSc", "S" -> "abc", "Ba" -> "aB", "Bb" -> "bb"}


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.