converting math problem into formal language question
in [Logic]
|
Prev: How can the MMx math be corrected?
Next: Is truth just something we have beliefs about or is there such a thing as truth?
From: Xah Lee on 20 May 2010 16:13 some interesting problem. Posted to sci.math but got no real answer. I'm looking for someone who can show me a example of modeling a math problem into a question in formal language. The example is at the bottom of of my blog here. the problem is written as a blog here ⢠Modeling Math Problem Into a Question in Formal Language http://xahlee.org/math/math_problem_into_formal_language.html plain text version follows: ------------------------------------ Modeling Math Problem Into a Question in Formal Language Xah Lee, 2010-05-19 Learned of The angel problem of John Horton Conway. Here's a rephrasing of the problem, perhaps easier to understand than the one given in Wikipedia: On a chess board of infinite size, suppose we place a king, call him the angel. And there's a devil. The angel and devil take turns. When it's angel's turn, he can move the king 2 times. When it is devil's turn, he can delete one square at any place. When a square is deleted, the king/angel will not be able to land on it. If the devil can delete enough squares completely surrounds the angel and is more than 2 steps thick, so that the angel cannot get out, the angel loses. Else the angel win. The above is called 2-angel problem, because the angel can move 2 steps in each turn. If the angel can move n steps in each turn, that problem is called n-angel problem. Note that when the angel makes a move, she can pass thru the deleted square, just can't land on it. So, in a n-angel problem, it is not enough for the devil to circle the angel with deleted squares, but the âwallâ must be n-thick. At first i don't quite understand the problem, but in trying to understand it, it grew on me. Not a trivial problem at all. (Conway is the one who created the âGame of Lifeâ cellular automata.) Be sure to read the original paper by John H Conway: The Angel problem (PDF) Apparently, it is not easy to prove that angel can win even if the angel can make 1000 steps in each turn. e.g. the 1000-angel problem. But it seems that the angel can win for n greater than 1. This is solved, proven, in 2006. However, as implied in Wikipedia, a explicit optimal strategy for the angel is not known. ------------------------------ Converting a Math Problem Into a Question in Formal Language One thing i wonder about these type of problems is that, how to create a model of it in mathematical logic? More specifically, how to turn this problem into a question with Formal language. For ease of explanation, let's focus on the specific 2-angel case. So, when turned into a formal language equivalent, the question would be something like whether a particular string is possible with a given formal language. I suspect that the process of turning such a problem as formal language problem, lots insights can be gained, though am not sure it helps deriving solutions. When this problem is modeled as a formal language, it may become convoluted and difficult to understand. However, i think it actually makes the problem the most simple, because it condenses the problem into its logical gist. And this is why, that many math problems that are simple to state that even a child can understand the question, yet are most difficult to solve. (e.g. many number theory problems and problems in recreational math) But really, when turned into its math gist, as a logic problem, in formal language, of a bunch of strings and transformation rules, and asking whether a given string is possible, one can see that these âsimpleâ problems are not simple to begin with, their real nature appears. Back to the 2-angel problem. Another interesting thing is how to represent the concept of optimal strategy in terms of a question in formal language? I have no idea... but i think it be represented as generating a particular shortest or longest string, of particular pattern. Or, perhaps the least number of steps to arrive at a given string. ------------------------------ Simple Example Problem To get started in this... i think it would be fruitful to start with a simple similar problem. Say, suppose you have a chess board, and the question is, is it possible to lay 3 pieces so that they form a line (horizontally or vertically)? Of course, this is trivial and even idiotic a question. Our job, is to formulate a equivalent problem in formal language. This way we'll learn what is involved. -------------------------------------------------- can anyone show me how this done in the last paragraph above? Thanks. Xah â http://xahlee.org/ â
From: George Greene on 21 May 2010 19:15 On May 20, 4:13 pm, Xah Lee <xah...(a)gmail.com> wrote: > Modeling Math Problem Into a Question in Formal Language Is this something that other people often do, or something that you are doing for the first time? I personally have never seen a math problem modeled into "a question in" formal language. Formal languages are sets of strings. The usual problem, in the context of ANY formal language, is simply to determine which strings belong to it and which do not. Please note that this DOES NOT involve any "question IN" the formal language. The formal language itself IS NOT a language IN WHICH "questions" can be phrased or posed, usually. It simply contains [some] strings [and not others]. Usually, each of these strings would be thought of as a STATEMENT or a (possible) SOLUTION to a problem, NOT A QUESTION. A string might also be a demonstration that a particular attempted solution fails. One obvious way to translate THIS problem into a formal language would be to just model any/every game as the string of its moves. But this would first require defining a finite alphabet for specifying moves. For the n- angel problem, the king's moves are easy to define from an alphabet with n symbols since there are always at most (2n+1)^2 places to which the king could move (from where he was previously). But there is no upper bound on "where" a devil-move could be (in terms of distance from any previous move), so those would have to be represented (in any alphabet) by arbitrarily long finite strings. Probably the easiest alphabet to use is one with 3 symbols -- 0,1, and a separation-symbol telling where the code for the previous move ends and the next move begins. You could then define a relevant formal language as consisting of all and only those strings in which the angel gets trapped, but that would be too simplistic since there is no way of separating (within these) those in which the angel was actually trying to escape, from those in which suboptimal moving allowed the angel to be caught even though (with better choices) it could have escaped. I don't even know if this is the direction you were intending to go, though, since you said "question". That almost invites thinking of a first-order logical language as a formal language and doing it that way (since that version of "formal language") is one in which every statement is also a question, especially if it is not a theorem or the negation of a theorem.
From: Charlie-Boo on 31 May 2010 14:01 On May 21, 7:15 pm, George Greene <gree...(a)email.unc.edu> wrote: > On May 20, 4:13 pm, Xah Lee <xah...(a)gmail.com> wrote: > > > Modeling Math Problem Into a Question in Formal Language > > Is this something that other people often do, > or something that you are doing for the first time? > > I personally have never seen a math problem modeled into "a question > in" > formal language. AI people tried it for years - things like the Tower of Hanoi puzzle. Problem-Solving Methods in Artificial Intelligence, Nilsson, 1971. Chapter 7. Application of the Predicate Calculus in Problem Solving C-B
From: George Greene on 1 Jun 2010 15:21 On May 31, 2:01 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > AI people tried it for years - things like the Tower of Hanoi puzzle. > Problem-Solving Methods in Artificial Intelligence, Nilsson, 1971. > Chapter 7. Application of the Predicate Calculus in Problem Solving I do NOT think predicate calculus and a first-order "formal language" are the kind of "formal language" that the OP had in mind. I think he was talking about a formal language as a set of strings (individual strings of which might be accepted or rejected by a TM).
From: Xah Lee on 1 Jun 2010 16:55
On Jun 1, 12:21 pm, George Greene <gree...(a)email.unc.edu> wrote: > On May 31, 2:01 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > AI people tried it for years - things like the Tower of Hanoi puzzle. > > Problem-Solving Methods in Artificial Intelligence, Nilsson, 1971. > > Chapter 7. Application of the Predicate Calculus in Problem Solving > > I do NOT think predicate calculus and a first-order "formal language" > are the kind of "formal language" that the OP had in mind. > I think he was talking about a formal language as a set of strings > (individual strings of which might be accepted or rejected by a TM). Yes George, that's correct. Thanks for your input in previous post. Though, i hoped there's more input. I'm pretty sure this has been explored. I'm rather not looking for a ad hoc solution to convert a particular mathematical problem into formal language... but am more looking for expert advices and materials... starting as a example, how to turn the question whether it is possible to align 5 chess pieces in a chess board. for example, there are lots of ways to turn a yes/no math problem into yes/no question in formal language. So, some natural question arise... which formal language is more efficient, how we judge, what are some general tips and methods to convert math into formal language...etc. (the goal i'm interested, is with respect to practical computability. i.e. once the problem is changed into a formal language question, that formal language should be easily implemented by computer, so that massive computing power can churn out theorems brute-force in hope to answer (Godel incompleteness theorems not withstanding... )) am looking for materials in this field. I'm pretty sure similar question have been explored in automated math proof system communities... am not professional mathematician or logician (am pro programer with amateur expertise in math and logic). I've wrote something here that may show why i'm interested in this: ⢠Math Notations, Computer Languages, and the âFormâ in Formalism http://xahlee.org/cmaci/notation/index.html > On May 31, 2:01 pm, Charlie-Boo <shymath...(a)gmail.com> wrote: > > > AI people tried it for years - things like the Tower of Hanoi puzzle. > > Problem-Solving Methods in Artificial Intelligence, Nilsson, 1971. > > Chapter 7. Application of the Predicate Calculus in Problem Solving cant find content or summary of that book or chapter online... is this general AI or does it touches on the formal language in a technical sense here? in any case, I'm sure today the field is quite different from the perspectives of 1971... any automated/assisted theorem provers experts care to comment? part of the question is... this has a lot to do with one school of math foundation, namely formalism and logicism. The ultimate goal is to turn whole math into formal language of strings. I read a few articles about theorem provers in 2008 ⢠State Of Theorem Proving Systems 2008 http://xahlee.org/cmaci/notation/theorem_proving_systems.html but haven't made my study far. I'm not sure, how these systems are close to formal language of strings, but i think in is very close, or perhaps modeled on the formal language of strings as much practical as possible? Xah â http://xahlee.org/ â On May 21, 4:15 pm, George Greene <gree...(a)email.unc.edu> wrote: > On May 20, 4:13 pm, Xah Lee <xah...(a)gmail.com> wrote: > > >  Modeling Math Problem Into a Question in Formal Language > > Is this something that other people often do, > or something that you are doing for the first time? > > I personally have never seen a math problem modeled into "a question > in" > formal language. > > Formal languages are sets of strings. > The usual problem, in the context of ANY formal language, is simply > to determine which strings belong to it and which do not. > Please note that this DOES NOT involve any "question IN" the formal > language. > The formal language itself IS NOT a language IN WHICH "questions" > can be phrased or posed, usually. > > It simply contains [some] strings [and not others]. > Usually, each of these strings would be thought of as a  STATEMENT or > a (possible) > SOLUTION to a problem, NOT A QUESTION. > A string might also be a demonstration that a particular attempted > solution fails. > > One obvious way to translate THIS problem into a formal language would > be to > just model any/every game as the string of its moves.  But this would > first > require defining a finite alphabet for specifying moves.  For the n- > angel problem, > the king's moves are easy to define from an alphabet with n symbols > since there > are always at most (2n+1)^2 places to which the king could move (from > where he was previously). > But there is no upper bound on "where" a devil-move could be (in terms > of distance from > any previous move), so those would have to be represented (in any > alphabet) by arbitrarily > long finite strings.  Probably the easiest alphabet to use is one with > 3 symbols -- 0,1, and a > separation-symbol telling where the code for the previous move ends > and the next move begins. > > You could then define a relevant formal language as consisting of all > and only those strings > in which the angel gets trapped, but that would be too simplistic > since there is no way of > separating (within these) those in which the angel was actually trying > to escape, > from those in which suboptimal moving allowed the angel to be caught > even though (with > better choices) it could have escaped. > > I don't even know if this is the direction you were intending to go, > though, since you said > "question".  That almost invites thinking of a first-order logical > language as a formal > language and doing it that way (since that version of "formal > language") is one in which > every statement is also a question, especially if it is not a theorem > or the negation of a theorem. |