Give it as input to a compiler and see if it gives an error message or not. Or apply the same trivial procedure compilers use: read it and look for a definition for every symbol that is not itself the left hand side of a definition.
It doesn't refer to any symbols, see in particular the difference between "world" and "world2", and notice that "world3" doesn't refer to "action()", but instead to "action2()", which you can assume to be a copy-paste of "action()"'s source code, with all the symbols renamed.
Ok, I think I see where our formalizations differ. In the formalization I'm using, the decision theory produces a strategy, which is a function that's given as an argument to the world program. The world program invokes the strategy zero or more times, each time passing in some arguments that give whatever information is available to the agent at some point, and getting back a (real or predicted) decision. The world program is completely self-contained; other than through the argument it receives, it may not contain references to the agent's choices at all...
Some people on LW have expressed interest in what's happening on the decision-theory-workshop mailing list. Here's an example of the kind of work we're trying to do there.
In April 2010 Gary Drescher proposed the "Agent simulates predictor" problem, or ASP, that shows how agents with lots of computational power sometimes fare worse than agents with limited resources. I'm posting it here with his permission:
About a month ago I came up with a way to formalize the problem, along the lines of my other formalizations:
Also Wei Dai has a tentative new decision theory that solves the problem, but this margin (and my brain) is too small to contain it :-)
Can LW generate the kind of insights needed to make progress on problems like ASP? Or should we keep working as a small clique?