Implementing a formal system in Python

Some of the contents of this post are contained in my third book.

In this post, we’ll go deeper into the syntactical part of a formal system, along with the semantical. We’ve discussed formal systems in the past, and in this post, we’ll get more practical by providing an implementation of an example formal system.

Example formal system in Python

Syntax

The syntax of the formal system that we’ll build, expressed in BNF (Backus-Naur form) is:

var  := "p" | "q" | "r"
expr := var | not expr | and expr expr | imp expr expr
prf  := proof expr

The code in Python that follows the same syntax is:

def Var(x): return {'children': [], 'expr': x, 'rule': 'var'}
def And(x, y): return { 'expr': 'and', 'rule': 'conj', 'children': [x, y]}
def Imp(x, y): return { 'expr': 'imp', 'rule': 'impl', 'children': [x, y]}
def Not(x): return {'expr': 'not', 'rule': 'neg', 'children': [x]}

We now have a way to represent some logical formulas, e.g. $p \land q$ as And(Var('p'), Var('q')).

Further, in our implementation, we also need a way to differentiate between well-formed formulas and theorems since not all well-formed formulas are theorems. For that, we provide the Proof data type and a way to extract a proof:

def Proof(x): return {'children': [x], 'expr': 'prf', 'rule': 'proof'}
def FromProof(x):
  if not isinstance(x, dict) or not 'children' in x or x['rule'] != 'proof': return None
  return x['children'][0]

Note that Proof(And(Var('p'), Var('q'))) ( $\vdash p \land q$ ) is different from And(Var('p'), Var('q')) ( $p \land q$ ). The former specifies a well-formed formula, while the latter an actual proof. The Proof constructor mustn’t be used directly; proofs should only be constructed given the rules that we provide next.

Semantics (inference rules)

def RuleSepL(x):
  if x['rule'] == 'proof': return Proof(FromProof(x)['children'][0])
  else: return None
def RuleSepR(x):
  if x['rule'] == 'proof': return Proof(FromProof(x)['children'][1])
  else: return None
def RuleFantasy(x, y):
  if not isinstance(x, dict) or not 'rule' in x or not callable(y): return None
  return Proof(Imp(x, FromProof(y(Proof(x)))))

The above implementation corresponds to the following rules, together with the implication introduction rule:

$\cfrac{A \quad B}{A \land B} (\texttt{RuleJoin}) \quad \cfrac{A \land B}{A} (\texttt{RuleSepL})$

RuleFantasy accepts a non-proven term x, whereas other rules accept proven terms; the hypothesis needn’t be necessarily true, it only states that “If this hypothesis were a theorem, then that would be a theorem”. The second argument is a function y that accepts a Proof and returns a Proof; basically, another rule which will be used to transform the hypothesis x. As a result, it produces the theorem $x \to y(x)$ .

For example, here’s how we can represent $\vdash p \land q \to p$ in Python:

>>> pprint.pprint(RuleFantasy(And(Var('p'), Var('q')), RuleSepL))
{'children': [{'children': [{'children': [{'children': [],
                                           'expr': 'p',
                                           'rule': 'var'},
                                          {'children': [],
                                           'expr': 'q',
                                           'rule': 'var'}],
                             'expr': 'and',
                             'rule': 'conj'},
                            {'children': [], 'expr': 'p', 'rule': 'var'}],
               'expr': 'imp',
               'rule': 'impl'}],
 'expr': 'prf',
 'rule': 'proof'}

More on syntax

We now have a way to construct syntactical terms and manipulate them using the inference rules. However, a more convenient approach would be to write a BNF parser; this will allow us to get rid of the functions Var/And/Not, but also it will allow for an easy way to convert a string to such objects, allowing for easy input from the user. That is, instead of manually writing the functions that construct syntactical terms, we rely on a grammar and an algorithm for a grammar parser.

Follows the implementation for the BNF parser in Python which is mostly based on my previous post:

def rule_match(grammar, expr, rule_name, partial = False):
  for rule in grammar[rule_name]:
    (process_next, rules_applied, expr_tok, rule_tok) = (False, { 'children': [] }, expr.split(' '), rule.split(' '))
    for token in rule_tok:
      # string has been consumed but not all rule rule_tok were rules_applied
      if expr_tok == []: process_next = True; break # proceed to next rule
      if token not in grammar:
        # treat literal as string since it's not defined in the grammar list
        if token != expr_tok[0]: process_next = True; break # proceed to next rule
        expr_tok.pop(0)
        rules_applied['expr'] = token
      else:
        # treat token as a grammar name
        [new_expr_tok, new_rules_applied, valid] = rule_match(grammar, ' '.join(expr_tok), token, True)
        if not valid: process_next = True ; break # proceed to next rule
        # skip adding empty nodes
        rules_applied['children'].append(new_rules_applied)
        # now that it's valid, use the new_expr_tok which is the remaining of the expr
        expr_tok = new_expr_tok
    # either the string is fully parsed, or this is a sub-call (we still have more stuff to parse)
    rules_applied['rule'] = rule_name
    if not process_next and (expr_tok == [] or partial):
      if not ('expr' in rules_applied): rules_applied = rules_applied['children'].pop()
      return [expr_tok, rules_applied, True]
  return [[], {}, False]

def grammar_match(grammar, expr):
  for rule_name in grammar:
    [ _, rules_applied, valid ] = rule_match(grammar, expr, rule_name)
    if valid:
      return rules_applied
  return False

We can now specify the exact same grammar as before, as follows:

grammar = {
  'var':  [ 'p', 'q', 'r' ],
  'neg':  [ 'not expr' ],
  'conj': [ 'and expr expr' ],
  'impl': [ 'imp expr expr' ],
  'expr': [ 'var', 'neg', 'conj', 'impl' ],
  'prf': [ 'proof expr' ],
}

Finally, here’s how we can prove the exact same thing we proved earlier ( $\vdash p \land q \to p$ ):

>>> foo = grammar_match(grammar, 'and p q')
>>> pprint.pprint(RuleFantasy(foo, RuleSepL))
{'children': [{'children': [{'children': [{'children': [],
                                           'expr': 'p',
                                           'rule': 'var'},
                                          {'children': [],
                                           'expr': 'q',
                                           'rule': 'var'}],
                             'expr': 'and',
                             'rule': 'conj'},
                            {'children': [], 'expr': 'p', 'rule': 'var'}],
               'expr': 'imp',
               'rule': 'impl'}],
 'expr': 'prf',
 'rule': 'proof'}

Conclusion

Formal systems lie at the heart of mathematics and computers. Similarly to constructing a programming language: we took some syntax, represented it in BNF, created a function that parses the BNF and creates an AST out of it, and we implemented the inference rules for transforming this syntax’s terms.

In programming languages like Lisp, you don’t even need to care about the syntax since you’re directly working with the AST. In Haskell, the keyword datatype is basically what allows you to create syntax. In Python, as we’ve seen, we need to write the algorithms for transforming the syntax from a string to an actual AST that can later be manipulated by the inference rules.

If all of this sounds interesting to you, you might enjoy my book as well 🙂 I also wrote a paper on a similar topic that you might find interesting.

The full code is available on this link.