FOM: expr. power of syntax

[Stephen Fenner]

On Fri, 19 Jul 2002, Steve Stevenson wrote:

> >From what I see, you can't parse ~~~~~~~x1 or ~(p->v). Your "var"
> definition doesn't have to be that restrictive.
>
> steve
>
Steve,

Thanks, I should be clearer; I was writing quickly off the top of my head.
Here's what ~~~~~~~x1 naively translates to, for example (ignore whitespace):

x2 := ~x1
x3 := ~x2
x4 := ~x3
x5 := ~x4
x6 := ~x5
x7 := ~x6
x8 := ~x7

Let's say that the value of the left-hand side of the last rule is the
value of the whole formula.  Any variable not occuring on the left-hand
side of ":=" is considered free.  If there is a circularity, then by
convention we can consider the value of the entire formula to be the
constant false.

We can express anything in propositional logic this way, up to a renaming
of the free variables.  So the "var" definition only needs to generate an
infinite supply of variable names.  This can of course be extended to
predicate logic.  This is the kind of translation that programming
language compilers do all the time.

>
>
>
> Stephen Fenner writes:
>  ...
>  > ...
>  >
>  > For propositional logic, consider the regular language given by the
>  > following rules (named regular expressions):
>  >
>  > digit  = 0|1|2|3|4|5|6|7|8|9
>  > number = {digit}{digit}*
>  > var    = X{number}
>  > neg    = ~{var}
>  > literal= {var}|{neg}|true|false
>  > conj   = {literal}&{literal} | {literal}
>  > disj   = {conj}v{conj} | {conj}
>  > rule   = {var}:={disj}
>  > formula= {rule}*
>  >
>  > [Here, "|" means union and "*" means Kleene closure and {name} means
>  > substitute the regular expression previously bound to that name.]
>  >
>  > The language is given by the last regular expression ({formula}).  Any
>  > propositional formula is computably translatable into a string in this
>  > language which preserves meaning and vice versa, given an appropriate
>  > semantics on the latter.
>  >
>  > Steve
>  >
>  >
>  >
>
>