What do you mean by "World: Strategy->Outcome"?
It means "World is the type of function that takes a Strategy as input and returns an Outcomes."
In the linked article, you've defined world, world2, and world3 as things that're not actually functions; they have unbound references to agent, which are parameters in disguise. You then show that if you mix parameters-as-unbound-references with real parameters, you can get confused into thinking they're independent. Which jus means you shouldn't use unbound references.
Which just means you shouldn't use unbound references.
How do you know that a given syntactic specification of a function doesn't "use unbound references"? Presence of a logical dependence on agent's action looks like something algorithmically impossible to detect. You can of course focus on a class of syntactic specifications that are known to not depend on agent's action (for example, GLUTs), but this is too restrictive for a FAI-grade decision theory that can handle the actual world, and ignores the problem of whether the process that specif...
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?