Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

My question is how to prove that $\Sigma$-formulas are uniquely readable (in our course this was wasn't really proved - in the proof it said just "proof by induction", but I'm confused what was meant by that, this we aren't dealing with numbers on which I can induct; was an induction by the length of the formula meant ? A colleague said,, that probably induction on the construction of the formula was meant, but I don't know what this menas either). I would very much like to see a proof, so that I can get the idea and use this type of proof later on my own, since a lot of "proofs by induction" which involve formulas follow...

Sadly, for this I have to introduce some definitions since they seem to vary from book to book and I haven't found a book, which uses similar definitions to the ones in your course (and since my questions are very much about the details, I can't use a different seet of defintions). So after these apologies, here comes the definition:

We have defined the set $\Sigma_{Term}$ of $\Sigma$-formulas as the smallest set of strings over the alphabet $\Sigma\cup\mathbb{V}$ (where $\Sigma$ is the signature and $\mathbb{V}=\left\{v_0,v_1,v_2,\ldots \right\}$ is a countable set of variables) such that:

$ \blacktriangleright$ every variable is a term

$ \blacktriangleright \ \ \ \mathtt{ft_1\ldots t_n}\in \Sigma_{Term}$ if $\mathtt{t_1,\ldots ,t_n}$ were $\Sigma$-terms and $\mathtt{f}$ was a symbol for a function of arity $n$ in the signature $\Sigma$

share|improve this question
    
Essentially the trick is to say that if you can uniquely read short formulae then you can uniquely read any conjunction/disjunction/etc. of shorter formulae. –  Asaf Karagila Jun 24 '11 at 9:26
1  
Each term and formula is either indivisible (e.g., a term that is simply a variable) or built from simpler elements according to well-defined rules (like the rule given above for constructing new terms). Induction on the construction of a term or formula entails checking that the indivisible objects all have the desired property and that the construction rules preserve the property. For more detail, search for the notion of 'structural induction'. –  Brian M. Scott Jun 24 '11 at 9:46
    
I think that if you try to rigorously formulate what is meant by unique readability (one obviously needs a rigorous definition to have a rigorous proof), you'll find that the proof is rather straightforward. –  Levon Haykazyan Jun 24 '11 at 10:37
1  
You've only told us how to build terms, but not how to build formulas, such as $(\varphi\wedge\psi)$ and so on, and the proof of unique readability depends on the specific details of how you do that. –  JDH Jun 24 '11 at 11:39
2  
Proving unique readability is different than most proofs about formulas. Most of those use structural induction, but you can't use that alone for proving unique readability, because the whole point of unique readability is to prove that there is only one way to recover structure from a string. In other words structural induction is generally used for things that have already been parsed. Proofs of unique readability often involve an induction on the length of the string, as in my proof below. –  Carl Mummert Jun 24 '11 at 12:23

1 Answer 1

up vote 6 down vote accepted

Your definition in the question just defines terms, not formulas. Here is how to prove unique readability of terms.

Say that a string $s$ encodes a sequence of terms if there is a sequence $t_1, \ldots, t_n$ such that $s$ is the concatenation of the string for $t_1$ followed by the string for $t_2$ and so on up to the string for $t_n$. Here I use "term" for the semantic object and "string" for the syntactic one being parsed.

Next, suppose for a contradiction that $s$ is a nonempty concatenation of nonempty strings representing terms which is of minimal length with respect to the property that $s$ can be parsed two ways, i.e., there are two different sequences of terms the concatenation of whose string makes $s$. In other words there is more than one way to parse $s$ into a sequence of terms, but no shorter string which encodes a sequence of terms has this property. If there is any string with that non-unique-readability property there is one of minimal length.

$s$ cannot be empty, there is only one way to parse that.

If $s$ starts with a variable then that variable must be the first term in any sequence of terms that makes up $s$, so the rest of $s$ must be able to be parsed in two ways, and the rest is a shorter string.

Thus we can assume $s$ starts with a function symbol $f$ of some arity $n$. Now look immediately after $f$. Because of the definition of terms, $f$ must be followed by a concatenation of strings for $n$ terms. So if we remove $f$ from the front of $s$ to get $s'$, then $s'$ is still a concatenation of terms ($n-1$ more terms than were in $s$, in a sense). Because $s$ was minimal, $s'$ can be parsed into a sequence of terms in only one way. But then $s$ also can be parsed into a sequence in only one way: the first $n$ terms of $s'$ go with $f$.

So the parsing algorithm is simply to repeat the following as long as the input is nonempty:

  • If you see a variable, take it from the input
  • If you see a function symbol, find its arity $n$, and then call this algorithm recursively to take $n$ terms from the input

When the input runs out, if you were in the middle of filling some function symbol's arguments, the string is invalid. Otherwise it is valid.

This sort of parsing algorithm is common for systems that use Polish notation, and its simplicity is one of their key advantages. Parsing for infix operators is much more difficult, because it requires parentheses to get unique readability.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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