On 9/14/21, [email protected] <[email protected]> wrote: > Hi YKY :) > > As for Tic Tac Toe, I believe this should work: write a winning strategy in > any functional language (being lambda calculus based). Then convert it to > logic rules by Curry-Howard correspondence. And voilà, you have a logic > representation of the winning strategy.
Yes, I'm glad you mentioned Curry-Howard. My objective here is to formulate a set of logic rules for Tic Tac Toe that is very "natural" and close to the way humans think about this game. For example, the human child will first learn the concept of 3-in-a-row, etc. Then he learns that "XX□" is almost 3-in-a-row, and is a "can win" situation. Then he learns that a "fork" is two distinct "can win" situations. Notice that the "fork" predicate is expressed with the "can win" predicate which is learned earlier (ie, more primitive). In other words, if we want to *re-use* earlier-learned predicates, we need to make *assumptions*, ie, imagined moves. By making imaginary moves we get back to the situations we have encountered *before*, instead of having to invent new concepts from scratch. In classical (ancient) logic-based AI, they have so-called ATMS (assumption-based truth maintenance systems) that keep track of assumptions and the conclusions they lead to. This makes the inference engine quite complicated. Curry-Howard can offer an interesting and perhaps useful insight: under Curry-Howard, an assumption in logic is just a variable. For example if we assume the proposition A, this corresponds to having a variable x:A of type A. When we create a proof making use of this assumption, this corresponds to having a function f, taking a proof of A to a proof of B. In other words, it is a λ-term "λx. f(x)". Notice that in this λ-term the variable x is bound and not free. This means that our proof has *discharged* the assumption A. Simon Thompson's book "Type Theory and Functional Programming" [1991] explains all this very nicely. > Other than Curry-Howard, from what I learned, logic represents a Turing > complete language, just use implication as a function symbol, and manage > variables in related predicates. We start from axioms (progressively > asserted Tic Tac Toe moves) that are raw material taken for granted, from > which all the conclusions in planing are deduced. When you check all the > branching conclusions, asserting all the possible opponent moves in between, > if you encounter a "win" combination, there could be a potential path for > winning if the opponent moves as predicted. This should work for any system, > including the Tic Tac Toe game. But beware, there could be an infinite loop > in rules, just like in regular programming, and it happens on recursive > implication. This could be avoided by tracking the recursion count, > rejecting high count branches. > > For Tic Tac Toe, just find a way to represent a board as a predicate system > (maybe one 9 parameters long, or three 3 parameters long, or whatever else > fits), define all the winning combinations, and that is half a job done. ------------------------------------------ Artificial General Intelligence List: AGI Permalink: https://agi.topicbox.com/groups/agi/T74958068c4e0a30f-Mca85424b4fc94610800e1dc4 Delivery options: https://agi.topicbox.com/groups/agi/subscription
