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