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 specified that GLUT could itself logically depend on agent’s action. (The very setup of a thought experiment could be controlled by an agent acting inside it, for example, for strange enough or sensitive-to-detail enough thought experiments.)
How do you know that a given syntactic specification of a function doesn’t “use unbound references”?
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.
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. The strategy is similarly self-contained; it receives no information about the world except through the arguments the world program passes to it. Then separately from that, a “decision theory” is a function that takes a symbolic representation of a world program, and returns a symbolic representation of a strategy.
Ultimately, this amounts to a refactoring; results that hold in one system still hold in the other, if you map the definitions appropriately. However, I’ve found that structuring problems this way makes the theory easier to build on, and makes underspecified problems easier to notice.
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.
Can you formalize this requirement? If I copy agent’s code, rename all symbols, obfuscate it, simulate its execution in a source code interpreter that runs in a hardware emulator running on an emulated linux box running on javascript inside a browser running on Windows running on a hardware simulator implemented (and then obfuscated again) in the same language as the world program, and insert this thing in the world program (along with a few billion people and a planet and a universe), how can you possibly make sure that there is no dependence?
Can you formalize this requirement? If I copy agent’s code … and insert this thing in the world program, how can you possibly make sure that there is no dependence?
You don’t get to do that, because when you’re writing World, the Strategy hasn’t been determined yet. Think of it as a challenge-response protocol; World is a challenge, and Strategy is a response. You can still do agent-copying, but you have to enlarge the scope of World to include the rules by which that copying was done, or else you get unrelated agents instead of copies.
To copy agent’s code, you don’t need to know strategy. World naturally changes if you change it, and the strategy might change as well if you run the agent on a changed world, but agent’s code is still the same, and you know this code. The new world will only depend on the new strategy, not the old one, but now we have a world that depends on its agent’s strategy, and you won’t be able to find how it does, if you don’t already know.
In any case, all this copying is irrelevant, because the point is that there can exist very convoluted worlds that depend on agent’s action, but it’s not feasible to know that they do or how they do. And we don’t get to choose the real world.
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.
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 specified that GLUT could itself logically depend on agent’s action. (The very setup of a thought experiment could be controlled by an agent acting inside it, for example, for strange enough or sensitive-to-detail enough thought experiments.)
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. The strategy is similarly self-contained; it receives no information about the world except through the arguments the world program passes to it. Then separately from that, a “decision theory” is a function that takes a symbolic representation of a world program, and returns a symbolic representation of a strategy.
Ultimately, this amounts to a refactoring; results that hold in one system still hold in the other, if you map the definitions appropriately. However, I’ve found that structuring problems this way makes the theory easier to build on, and makes underspecified problems easier to notice.
Can you formalize this requirement? If I copy agent’s code, rename all symbols, obfuscate it, simulate its execution in a source code interpreter that runs in a hardware emulator running on an emulated linux box running on javascript inside a browser running on Windows running on a hardware simulator implemented (and then obfuscated again) in the same language as the world program, and insert this thing in the world program (along with a few billion people and a planet and a universe), how can you possibly make sure that there is no dependence?
You don’t get to do that, because when you’re writing World, the Strategy hasn’t been determined yet. Think of it as a challenge-response protocol; World is a challenge, and Strategy is a response. You can still do agent-copying, but you have to enlarge the scope of World to include the rules by which that copying was done, or else you get unrelated agents instead of copies.
To copy agent’s code, you don’t need to know strategy. World naturally changes if you change it, and the strategy might change as well if you run the agent on a changed world, but agent’s code is still the same, and you know this code. The new world will only depend on the new strategy, not the old one, but now we have a world that depends on its agent’s strategy, and you won’t be able to find how it does, if you don’t already know.
In any case, all this copying is irrelevant, because the point is that there can exist very convoluted worlds that depend on agent’s action, but it’s not feasible to know that they do or how they do. And we don’t get to choose the real world.