Re: [sl4] Rolf's gambit revisited

From: Benja Fallenstein (benja.fallenstein@gmail.com)
Date: Tue Jan 06 2009 - 10:42:27 MST


I wrote:
> I don't want to try my hand at doing this with Turing machines, but
> let's try it with computable functions.
(...)

For those who read Haskell, below is a type-checked version of the
definitions and claims in my previous message.

- Benja

=====

{-# LANGUAGE EmptyDataDecls #-}

import Prelude hiding (interact)
import Control.Arrow (first)

-- Rep (a -> b) = Gödel number
-- Rep (x,y) = surjective pairing of representations of x and y
-- Rep Input/Rep Action/Rep Message = natural number representing inp/act/msg
data Rep a

pair :: (Rep a, Rep b) -> Rep (a,b)
unpair :: Rep (a,b) -> (Rep a, Rep b)
pair = undefined; unpair = undefined

tuple :: (Rep a, Rep b, Rep c, Rep d, Rep e, Rep f) -> Rep (a,b,c,d,e,f)
untuple :: Rep (a,b,c,d,e,f) -> (Rep a, Rep b, Rep c, Rep d, Rep e, Rep f)
tuple = undefined; untuple = undefined

eval :: Rep a -> a
eval = undefined

apply :: Rep ((a,b) -> c) -> Rep a -> Rep (b -> c)
apply = undefined

fixRep :: (Rep (a -> b) -> (Rep a -> Rep b)) -> Rep (a -> b)
fixRep = undefined

data Input; data Action
newtype Agent = Agent { runAgent :: Rep Input -> (Rep Action, Rep Agent) }
newtype Env = Env { runEnv :: Rep Action -> (Rep Input, Rep Env) }

mkAgent :: (Rep (Input -> (Action, Agent))) -> Rep Agent
mkAgent = undefined

interact :: Rep Agent -> Rep Input -> Rep Env -> [(Rep Input,Rep Action)]
interact ag inp env = (inp,act) : interact ag' inp' env' where
    (act,ag') = runAgent (eval ag) inp
    (inp',env') = runEnv (eval env) act

data Message
type MsgInput = (Message, Input)
type MsgAction = (Message, Action)
newtype MsgAgent = MsgAgent { runMsgAgent :: Rep MsgInput -> (Rep
MsgAction, Rep MsgAgent) }

interactMsg :: Rep MsgAgent -> Rep MsgAgent
            -> Rep Input -> Rep Input
            -> Rep Message -> Rep Message
            -> Rep Env -> Rep Env
            -> [(Rep Input,Rep Input,Rep Message,Rep Message,Rep
Action,Rep Action)]
interactMsg ag1 ag2 inp1 inp2 msg1 msg2 env1 env2 = result where
    result = (inp1,inp2,msg1',msg2',act1,act2) : rest
    rest = interactMsg ag1' ag2' inp1' inp2' msg1' msg2' env1' env2'
    ((msg1',act1),ag1') = first unpair $ runMsgAgent (eval ag1) (pair
(msg1,inp1))
    ((msg2',act2),ag2') = first unpair $ runMsgAgent (eval ag2) (pair
(msg2,inp2))
    (inp1',env1') = runEnv (eval env1) act1
    (inp2',env2') = runEnv (eval env2) act2

rolfinize :: Rep MsgAgent -> Rep MsgAgent
          -> Rep Input
          -> Rep Message -> Rep Message
          -> Rep Env
          -> Rep Agent
rolfinize ag1 ag2 inp2 msg1 msg2 env2 = mkAgent (apply (fixRep rolf') tup) where
    tup = tuple (ag1,ag2,inp2,msg1,msg2,env2)

rolf' :: Rep (((MsgAgent,MsgAgent,Input,Message,Message,Env),Input) ->
              (Action, Agent))
      -> Rep ((MsgAgent,MsgAgent,Input,Message,Message,Env),Input)
      -> Rep (Action, Agent)
rolf' r arg = pair (act1, ag1star') where
   (tup,inp1) = unpair arg
   (ag1,ag2,inp2,msg1,msg2,env2) = untuple tup
   ((msg1',act1),ag1') = first unpair $ runMsgAgent (eval ag1) (pair
(msg1,inp1))
   ((msg2',act2),ag2') = first unpair $ runMsgAgent (eval ag2) (pair
(msg2,inp2))
   (inp2',env2') = runEnv (eval env2) act2
   ag1star' = mkAgent (apply r (tuple tup'))
   tup' = (ag1',ag2',inp2',msg1',msg2',env2')

data Proposition

equals :: a -> a -> Proposition
equals = undefined

forAll :: (a -> Proposition) -> Proposition
forAll = undefined

theorem :: Proposition
theorem = forAll $ \(ag1,ag2,inp1,inp2,msg1,msg2,env1,env2) ->
  let xs = interact (rolfinize ag1 ag2 inp2 msg1 msg2 env2) inp1 env2
      ys = map f (interactMsg ag1 ag2 inp1 inp2 msg1 msg2 env1 env2)
      f (i1,i2,m1,m2,a1,a2) = (i1,a1)
   in xs `equals` ys

main = putStrLn "It type-checks, but is it true?"



This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:01:03 MDT