Functions are degenerate Relations. Anyone that starts from a functional programming perspective has already lost the war.
Here's a question for ya'll: What is the Relational generalization of Curry-Howard? On Sat, Sep 18, 2021 at 10:09 AM YKY (Yan King Yin, 甄景贤) < generic.intellige...@gmail.com> wrote: > On 9/14/21, ivan.mo...@gmail.com <ivan.mo...@gmail.com> 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-Ma5a6365ef5649312927ea6d4 Delivery options: https://agi.topicbox.com/groups/agi/subscription
