In an earlier notebook, we exhibited travesties and bidirectional parsing tools for algebraic formulas (https://community.wolfram.com/groups/-/m/t/3094266). We extend those methods to cover two more examples: symbolic logic and programming-language types. The algebra example is repeated here for completeness. We illustrate symbolic logic via the famous game, “WFF-n-Proof.” “WFF” stands for well-formed formula, and the game employs an alternative notation for Boolean logic. Physical copies of the WFF-n-Proof manual by Layman Allen (https://paw.princeton.edu/memorial/layman-edward-allen-51) are abundant online (e.g., https://a.co/d/aiQM1H2). The work is still copyrighted. Digital copies are not legally available. In this notebook, I refer to page numbers etc. from the 1965 manual without reproducing them verbatim. We illustrate programming-language types via examples from Benjamin C. Pierce’s book, Types and Programming Languages (https://a.co/d/9ofcYh4). In addition to generating travesties and parsing tools, we exhibit abstract execution for these domains. We execute well-formed formulas (WFFs) via logic programming and execute typed programs via small-step operational semantics.

Preliminary Packages

In[]:=
<<Utilities`CleanSlate`
If you like, move the following packages onto your Mathematica $Path. The following unevaluatable cell shows where I put them on my system. I include copies of these packages here so anyone can just evaluate this notebook without installing packages. We don’t explain this code, here, we just use it. Close up this chapter so you don’t have to look at all this stuff.
In[]:=
<<"~/Dropbox/MMA/Packages/JacquardProlog.m"​​<<"~/Dropbox/MMA/logic.m"​​<<"~/Dropbox/MMA/Packages/Jacquard.m"

logic.m


Jacquard.m


JacquardProlog.m


Polish Prefix Grammars

Our Polish prefix grammars (PPFs) are of the form [non-terminal] [some-fixed-number-of-arguments]. Such grammars are easy to parse, and it’s easy to automatically generate parsers for such grammars.

Definitions

Definitions are in bold italics.
Let a grammar be a function from non-terminal symbols to productions, each of which is a list as a suit (permutation, ordered, no duplicates) of alternatives. Alternatives are ordered for zipping them with travesty-generation probabilities. Logically, alternatives are unordered, i.e., a set rather than a suit.
The productions of a context-free grammar pertain anywhere in an utterance without regard to preceding or following input. Such grammars are the only ones of interest, here.
Each alternative is a list, as a sequence (ordered, duplicates allowed), of terms. The terms in an alternative must match, in both order and form, the terms in utterances.
A term is either a terminal symbol or a non-terminal symbol.
A terminal symbol is a literal — a Symbol, String, or a Number — that must match exactly a token appearing in the input.
A non-terminal symbol is any term in the grammar that is not a terminal symbol. A non-terminal symbol recurses back into the grammar. It’s always of Mathematica type Symbol.
A production is a suit of alternatives.
A token is a symbol, string, or number, for example, containing an atomic utterance of the language of interest. In WFF-n-Proof, our first motivating example, a token is a single character.
An utterance is a list (as a sequence) of terminal symbols.
The start symbol is the special, distinguished name and symbol Start, not available for other uses.

WFF-n-Proof

The following is an example of a PPF grammar from the famous game “WFF-n-Proof.” We’ll generate travesties, parsers, antiparsers, unparsers, and even resurrect a couple of old Prolog simulators by Cabrera and Jabelean to process inference rules from the game. This is a big example. It illustrates all our syntax-driven machinery. Once that machinery is developed, however, we re-use it without modification on algebraic expressions and on types for programming languages.
In[]:=
ClearAll[P,WFF,Proposition,Unary,Binary,T,nonTerminalsFromGrammar,terminalsFromGrammar];
We represent suits (permutations), sets, bags, and lists as lists in Mathematica.

P = Suit of Productions = Grammar

NOTE: We never refer to Global Variables in function bodies. That’s dangerous because their values may change willy-nilly. Instead, all our functions take all data through parameters. Our Global Variables represent specific examples like WFF-n-Proof, and those Global Variables may appear as actual arguments when calling functions.
P is a list (as a suit of productions) of lists (as alternatives, i.e., as sequences of terms).
A WFF is either a Proposition, a Unary, or a Binary:
In[]:=
P[WFF]=
Proposition
Unary
Binary
;
A Proposition is any one of the four terminal constants
p
,
q
,
r
,
s
.
In[]:=
P[Proposition]=
"p"
"q"
"r"
"s"
;
A Unary — the language has only one Unary — is a terminal
N
for NOT followed by a WFF.
In[]:=
P[Unary]=(
"N"
WFF
);
The language has four Binaries:
C is Conditional
A is not And, it’s OR!
K is Konjunction (it’s AND)
E is Equivalence
In[]:=
P[Binary]=
"C"
WFF
WFF
"A"
WFF
WFF
"K"
WFF
WFF
"E"
WFF
WFF
;
The magical Start symbol is just a WFF:
In[]:=
P[Start]={{WFF}};
Double-check:
In[]:=
??P
Out[]=
Symbol
Global`P
Definitions
P[WFF]={{Proposition},{Unary},{Binary}}
P[Proposition]={{p},{q},{r},{s}}
P[Unary]={{N,WFF}}
P[Binary]={{C,WFF,WFF},{A,WFF,WFF},{K,WFF,WFF},{E,WFF,WFF}}
P[Start]={{WFF}}
Full Name
Global`P
​

NT = Set of Non-Terminals

“DownValues” sniffs the domain (non-terminals) of a tabular function-definition like P.
In[]:=
DownValues[P]//TableForm
Out[]//TableForm=
HoldPattern[P[Binary]]{{C,WFF,WFF},{A,WFF,WFF},{K,WFF,WFF},{E,WFF,WFF}}
HoldPattern[P[Proposition]]{{p},{q},{r},{s}}
HoldPattern[P[Start]]{{WFF}}
HoldPattern[P[Unary]]{{N,WFF}}
HoldPattern[P[WFF]]{{Proposition},{Unary},{Binary}}
How about a pretty display? In gridRules from the Jacquard package above, terminals are in dark red, non-terminals in dark blue. Lists are green boxes. Lists of lists are doubled green boxes. This visual notation does not distinguish lists as suits, sets, sequences, or bags. Rules have orange boxes on the left and light-yellow boxes on the right.The following displays the rules above.
In[]:=
Module[{d=DownValues[P]},​​Zip[​​Function[hp,hp[[1,1,1]]]/@Unevaluated/@d,​​Function[hp,hp[[1,1]]]/@d,Rule]]//
gridRules
Out[]=
Binary
C
WFF
WFF
A
WFF
WFF
K
WFF
WFF
E
WFF
WFF
Proposition
p
q
r
s
Start
WFF
Unary
N
WFF
WFF
Proposition
Unary
Binary
Sniff out the non-terminals.
Out[]//InputForm=
{Binary, Proposition, Start, Unary, WFF}

T = Set of Terminals

The terminals in a grammar is the complement of the non-terminals against the set of all symbols, which is the union of all the right-hand sides of the productions.
In gridExpression from Jacquard, terminals are in a light-yellow background, non-terminals in a purple background; gridExpression is a visual FullForm, so it shows the Head List explicitly, whereas gridRules, as above, exhibits lists as colored boxes without the explicit Head List.
InputForm is another way to visualize data. It adds back in the double quotes around Strings.
Sniff out the terminals.

Anti-Parsing: Syntax-Driven Travesties

We’ll do travesties before parsers so we can use travesties to test parsers.

Inject Probabilities into the Grammar

Transform each alternative (sequence of terms) into a list of rules, one rule for the probability of choosing the alternative in a travesty and another rule for the original alternative itself. Generate the probabilities with a given function that maps the alternatives to a parallel, isocardinal (zippable) list. The orders of the alternatives and of the probabilities are important only for Zip. The alternatives are, notionally, a set.
The following function assigns equal probabilities to every element of a list. It’s the default. Use something else if you have better estimates of appropriate probabilities. We’ll see an example of that in BPTProbabilities below for Benjamin-Pierce types.

iP = set of probabilized productions

Productions (headed by non-terminals) with injected probabilities.
Examine them (DownValues doesn’t Evaluate its arguments by default, so we must).
Something more pretty to look at? In here, “probability” and “alternative” are strings as keys in lookup tables. They’re not terminals in the grammar because they’re inside orange boxes, where keys always go in gridRules.

Choose From Alternatives

A function from probabilized alternatives to a particular choice, given an input die roll.

Case: One Alternative

If there is only one alternative (no rest___ in the pattern), choose that alternative. Access the key “alternative” in the lookup table by applying the rules via /., ReplaceAll.

Case: Many Alternatives

If there are many alternatives, pick the first whose cumulative probability is greater than or equal to the dieRoll. Track the cumulative probability by decrementing the dieRoll by each probability while recursing down the alternatives.

generateSentences [ probabilizedGrammar, groundTerm, terminalSymbols, recursionLimit:100 ]

The ground term is the term to force when the recursion limit is exceeded. The default recursion limit is 100. 500 is a useful value for this limit, later.

debugPrint: helper

It’s debatable whether to have a symbol like debugPrint for Print debugging, or to use Block[{Print=Identity},...] to switch off printing.

chainExpansion

Iterate down the terms, randomly choosing a branch to explore.
Case: exhausted the production:
Case: found a term in the production
Case: exceeded the recursion limit

generateSentence [ iP, groundTerm, T, recursionLimit ]

The following historically generated bugs. Keep it around as a regression test.

expressionStringFromSentenceRules

Just in case we want to transform terminals in the grammar to something else, for example, for putting in a lexical separator.

Interactive Test Samples

Press the button as many times as you like to see new Well-Formed Formulae.
Animate is a funny beast: the expression being evaluated must depend on the iteration variable, u in this case, or nothing happens. We make an artificial dependency.
Here’s the biggest one found so far.

randomUtterance [ ]

This seed historically exposed bugs, so we keep it around.

Parsing

Given an utterance, build a tree of the non-terminals that generate it.
We’ll first create a hard-coded parser for the WFF language, then we will create a machine-generated parser and compare the two parsers. The machine-generated parser results from a parser-generator that can write a parser from any PFF grammar.

Hard-Coded, Recursive-Descent Parser (Ground Truth)

This parser is hard-coded to our grammar.
First, tokenize the utterance. In our example, tokenizing is trivial because each token is a single character.
Mathematica has a built-in named “Alternatives” for pattern-matching. It has nothing to do with alternatives in our grammar.
Our parser transforms a list of tokens and a tree into a new list of tokens and a tree. The parser consumes one or more tokens and recursively builds up the tree. If there are no tokens, the parser returns the tree.
Check out the parses of generated sentences by pressing the button below:

Data-Driven Parsing

Can we write parserFromGrammar, a function that writes a parser from a grammar? We want such a thing because (1) it saves us work and (2) it’s reusable on any PPF grammar.
Here is a parser generator that will work on any PPF grammar, without left-recursion, of fixed-arity prefix forms.
Inspect a grammar

prefix,
suffix,
terminalsFromRule,
nonTerminalHeadFromRule,
arityFromPrefixRule

genParserBody, parserDefFromGrammarRule

For arity-0 productions:
Recurse for productions with right-hand sides
Accumulate overloads of parserTargetSym: for each set of terminals in a rule, write a Mathematica pattern to recognize those Mathematica Alternatives (“firstPattern” below).
Build up a parser table from that grammar by side-effecting parserTable.
Ad-hoc symbol, $parse, for a new machine-generated parser. Build the parser by scanning parserDefFromGrammarRule over all the rules in the grammar:
Compare the hand-written parser parse to the machine-generated parser $parse on random inputs (now you see why we did travesty generation before parsing — so we can test parsers!).
The machine-generated parser is about 50% slower than the hand-written parser, but that’s offset by the engineering factors that we didn’t have to write the machine-generated parser by hand and that we can reuse the machine-generated parser on other PPF grammars.

parseWFF

Save the machine-generated parser for WFF in a convenient, top-level function.
Reminders on some constituent functions:

$p: a Handy Composition

Unparsing

Unparsing is building utterances from trees. We need this for round-trip testing of parsers.

By Hand

Example:
Counterexample:

Machine-Generated

genUnparserBody, unparserDefFromGrammarRule

Ad-hoc Test

Stress Test

Generate random utterances (travesties), parse them, unparse the parse, check for equality.

WFF-N-Proof Inference Rules

Start on page 34 of the WFF-n-Proof book.
Produce a set-as-list of inferences from a term.

Outgoing Rules

mnemonic: “K” is “Konjunction”

Notice, And is NOT orderless (commutative), so we must introduces all combinations of rules to accommodate various proofs(!). We could replace it with an Orderless “WFFAnd”, but this would not allow us to prove, for example, “Ksr” because Mathematica's canonicalization will always rewrite it as “Krs”. A small point, but absent a proof or hypothesis that Kxy is equivalent to Kyx, we can’t tolerate this.
Build a table of names from parsed forms for display.
Rule “Ko” says that the two arguments, x, and y, of a Conjunction Kxy, are separately true. For example, Kpq implies p and implies q.
Because “And” is not part of our “object language,” WFF, we actually need two rules. This also eliminates the indeterminacy inherent in the actual definitions in WFF-n-Proof.
pages 37-40
Examples
Parse “Kpq,” then apply “Ko.”
Pick just the left branch.
parse, infer, unparse:

mnemonic: “C” is “Conditional”

The following, CoL and CoR, are not proper rules of inference according to the usual interpretation of Condition, but they are useful for examples 2 and 3 on page 90 of WFF-n-Proof.
Let CLR stand for any term like Cpq, where L=p and R=q.
If we are given ONLY CLR and R, can we deduce L? Not from Co. Co lets us deduce R from CLR and L but not L from CLR and R. However, we can say, from CLR and R, that L is a possibility — a possible solution to the following problem: “Given CLR and R, is there some L such that CLR and L implies R, and if so, what is this L?” In other words, L is consistent with CLR and R; L does not produce a contradiction.

Directed Rules CoL and CoR are Not Inference Rules

Write a directed rule, CoL, that solves the problem of finding an L that implies R given CLR. Later, we write a generic solver and discard these directed rules.
Do not apply directed rules in an inference. Instead, use them to search for solutions.
A related problem is “Given L and R, can we find a rule involving C such that CLR obtains?” This is not an inference, but a possibility. We can’t deduce CLR from L and R, but we can say that CLR is consistent with L and R.
Examples
Inference in the forward direction.
No inference backwards (Co is like a diode).

mnemonic: “A” is not AND, it’s OR!

The combinatorics on this one are annoying — arguing that we would really like an Orderless version of And, but we can’t tolerate an orderless And without an infix operator, and we don’t want that.

mnemonic: “N” is “Negation”

Twisted Modus Tollens (“not q” and “p implies q” means “p” is false); negation on the left

mnemonic: “E” is “Equivalence”

“p” implies “q” and “q” implies “p”.

Incoming Rules

Produce grammatical terms from parts
Modus Tollens (“p” implies “q” and “not q” means “p” is false).
Equivalence

Examples

Example 1:

just a parse
a logical statement outside the grammar
Put it back in the grammar by an Incoming Rule.
Unparse, completing the round-trip.

Example 2 (ex 1 on page 37 of WFF-n-Proof):

Example 3 (ex 6 on page 37 of WFF-n-Proof):

Experiment with Cabrera’s solver

A limitation of Cabrera’s solver is that it eagerly expands rules into facts, explosively, perhaps even infinitely, consuming memory. Until we make this lazy, we’ll use Jabelean’s solver, which is slower than Cabrera’s because it does not use Mathematica’s pattern matching.

Back to Jabelean’s solver

This next shows that the solver is bi-directional:
The next two show similar solutions for different L and R terms in a CLR.

Example 8 (3 on page 90 of WFF-n-Proof)

Can we find a CLR given an L and an R?
We can find all CLRs in the fact base, then filter them down to the ones that match our given L and R. We’ll do the filtering with a post-processing phase, to the solver. The solver’s job is to give us all CLRs in the fact base.
We can also do it much faster and shorter by the direct but “out-of-the-box” pseudo-inference rule CoR:

Page 91 of WFF-n-Proof

The first one is a proper application of the true inference rule Co:
The second one requires a solution, that is, finding a CLR and L that would imply R
Or writing it all out
We can do the same with the bogus pseudorule CoR
The third one also requires a solution:
or an application of the bogus pseudorule CoL

Proofs (page 92 ff)

P1 — page 92

Deeper Deductions

P2 — page 103

P3 — page 110

Reiteration — page 119ff

Do a better job of laying out proofs; page 122ff
Here’s an approach to the sequences, but it creates difficulties for the justifications.
Suppose we know at the outset how many levels of nesting we need. we can then use SpanFromLeft to leave judicious spacing.
There’s the pattern I like best.

Algebra-1 Travesties

This section is reproduced from an earlier notebook, and included here for completeness.
Let’s generate travesties for expressions in basic algebra. Such travesties might serve us well for testing an expression parser. A generative grammar for the expressions is one of our PPFs, however. We don’t need any new machinery. This example works just as well as WFF-n-Proof.
Biggest one found so far:

Ben Pierce Types

Encode types from Benjamin C. Pierce’s book, TPL or “Types and Programming Languages.”
Call the grammar “BPT,” for “Ben Pierce Terms,” from Section 3.1 of his book. It has ONE non-terminal symbol. He calls it “t.” That’s too small for us. We’ll call it “Term.”

Untyped Utterances

Consistent with Sections 3.2 and 4.1 of TPL.
BP’s Ternary if foo then bar else baz is not in Polish prefix form. Prefix form would be if foo bar baz, much easier to parse with our nearly-trivial tools. Go there, because the point of this exercise is not to spend time on parsing, but to spend time on types.
from Section 4.1:
Generate some travesties from this grammar, BPT. Equiprobabilities doesn’t generate enough variety, so we’ll build a probability-assignment function up by hand.
The parser, itself, is a composition of partTree (‘cadr’), the parser table above, and a tokenizer function, which will just be StringSplit for this application:
In the display below, hover over a vertex to see its content.

Small-Step Operational Semantics

Gin up a sample.

Boolean Evaluation Rules

The function for boolRules can be called with complicated arguments:
The following is the derivation tree of Section 3.5.3 in an manually prettified input form. But the output is clear.

Numerical Evaluation Rules

Some travesties on NB
Cross the syntactic domain of BPT[Term] into the syntactic domain of NB[Nv].
Above exercise 3.5.14:

CITE THIS NOTEBOOK

Travesties for Logic and for Types​
by Brian Beckman​
Wolfram Community, STAFF PICKS, January 29, 2024
​https://community.wolfram.com/groups/-/m/t/3111879