3
$\begingroup$

How to encode a first order formula into binary string, which I could give as input to Turing machine or program to do something with it (deciding is it satisfiable, or is concrete structure model for it, for example)?

I've read that I should first make a tree (which I know how to do) and then encode that tree, which I don't know how to do and I don't understand why I need to make that tree? Why don't just make binary number for every symbol which could appear in formula $( = , \vee, \wedge, <=>, =>, \exists, \forall...)$ and connect them into string for concrete formula?

| cite | improve this question | |
$\endgroup$
2
$\begingroup$

There is one encoding scheme which is particularly obvious. Under this encoding scheme, the encoding of the formula $a \Rightarrow (b \Rightarrow a)$ is $$ a \Rightarrow (b \Rightarrow a). $$ A C program can parse this string into a tree if it needs to, but it's up to the program.

It is of course possible to think of many other encoding schemes, but unless you are interested in very weak complexity classes, the exact encoding scheme doesn't matter.

There is one fine point here: the alphabet is finite, but there could be formulas with arbitrarily many variables. There are many ways to solve this problem. For example, you can name variables in the form "$v$ + number", for example $v5$, $v107$, and so on. This uses only a finite alphabet (since we encode the number in decimal, using 10 symbols).

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thank you a lot for answer. I wanted to know how to represent a formula, for example formula you have written in comment, in binary string, just with 0s and 1s. I'm learning about finite model theory and its connection to complexity classes, and I've understood how to represent a structure by representing number of elements and its relations by binary string, but I can't figure out how to write a formula in zeros and ones. I need to, for example, offer a code of structure and a code of formula to Turing machine and program it to decide if structure is model for formula. $\endgroup$ – Betelgez Apr 5 '17 at 22:48
  • $\begingroup$ Every alphabet can be converted to binary, in the same way that plain text files use ASCII. Just use some prefix code for your alphabet. $\endgroup$ – Yuval Filmus Apr 6 '17 at 4:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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