I’m getting serious about decision theory. I have some foundational observations, upon which I’m building a mathematical framework. I have some partial drafts, and plan to write papers on it.
Most problems in decision theory are the result of insufficient rigor. “Rigor” to me means formalizing problems fully and proving things about the formalization, without use of fuzzy language. Full formalization means writing out the problem statement as two type-checkable functions, a world function which maps strategies to outcomes and a preference function which defines an ordering over outcomes. To my knowledge, none of the decision theory in the literature is done at this level of rigor. I have chosen a subset of SML/NJ, extended to include limiting expressions, as the representation for formalized problems, because it has solid mathematical foundations with which I am already familiar, and also a rigorous model of partial evaluation.
There is a pre-existing body of work on how to prove things about programs and transform and simplify them in provably correct ways in computer science: compiler theory. One of the major themes I’ve picked up from studying compilers is that different representations enable us to prove different things and perform different operations. In practice every compiler takes programs through a long series of intermediate representations. One of these representations, Static Single-Assignment (SSA) form, is strongly analogous to Pearl’s causal models. Another representation, continuation-passing style (CPS), enables a natural and precise statement of one interpretation of causal decision theory, along with a precise description of when it does and doesn’t work, such that you could prove that CDT is valid for a particular problem as a lemma and then apply CDT to it.
I haven’t proved it yet, but I think I can prove within the framework I’ve defined that Eliezer’s answer to the Prisoner’s Dilemma, “cooperate iff your opponent cooperates iff you cooperate”, is uncomputable, and that there is an infinite series of successively better approximations such that the Prisoner’s Dilemma has no optimal answer.
This isn’t really that important, but do you know if anyone has actually shown in a rigorous way that CDT two-boxes on Newcomb’s problem?
No one has, because CDT isn’t rigorous enough to bring into a proof framework without first disambiguating it, and there is at least one disambiguation that one-boxes and at least one disambiguation that two-boxes.
“Cooperate iff your opponent cooperates iff you cooperate” is impossible if your opponent always defects. (If you defect, “your opponent cooperates iff you cooperate” is true, so you should’ve cooperated :-) Eliezer pointed that out to me a while ago.
Regarding your overall approach, choosing a specific programming language feels like a wrong step to me. At some point you will want your results to have applicability in the wider world of Turing machines and algorithms, so why not start there? It’s not fuzzy at all and people have proved a lot of rigorous stuff about Turing machines.
“Cooperate iff your opponent cooperates iff you cooperate” is impossible if your opponent always defects. (If you defect, “your opponent cooperates iff you cooperate” is true, so you should’ve cooperated :-) Eliezer pointed that out to me a while ago.
The linked comment seems wrong—due to fuzzy language, ironically enough. The inner iff should be testing a counterfactual, not equality. That doesn’t help with the infinite regress/computability issue, though.
Anyways, I’ve found a specific probability distribution of opponents that reads your source, checks for the presence of a sufficiently large number and makes playing PD against them reduce to the name-your-utility game. And I can transform any set of agents into a set of agents that is a Nash equilibrium, by prepending a test for whether the opponent is a member of that set, and cooperating if so.
I still don’t know whether there’s an optimal solution for PD against agents drawn from any really complex distribution like the Solomonoff prior, or against agents iteratively selected starting from the universal prior. I suspect I could construct degenerate Solomonoff-like priors that force it to have or not have an optimal solution.
Regarding your overall approach, choosing a specific programming language feels like a wrong step to me.
I realized that yesterday when I first tried moving my examples into an actual compiler, and found that the language I’d chosen was not quite what I remembered, in ways that could be summarized as “the language is broken”. So I suspect I’m going to be making up yet another a language. I’d rather not use notation loosely, though.
At some point you will want your results to have applicability in the wider world of Turing machines and algorithms, so why not start there? It’s not fuzzy at all and people have proved a lot of rigorous stuff about Turing machines.
If you mean I should talk about Turing machines, no way. Compare the strength of what you can prove about a program that you take through a functional representation and various augmented SSA forms, to what you can prove about Turing machines, and the difference is enormous.
I’m getting serious about decision theory. I have some foundational observations, upon which I’m building a mathematical framework. I have some partial drafts, and plan to write papers on it.
Most problems in decision theory are the result of insufficient rigor. “Rigor” to me means formalizing problems fully and proving things about the formalization, without use of fuzzy language. Full formalization means writing out the problem statement as two type-checkable functions, a world function which maps strategies to outcomes and a preference function which defines an ordering over outcomes. To my knowledge, none of the decision theory in the literature is done at this level of rigor. I have chosen a subset of SML/NJ, extended to include limiting expressions, as the representation for formalized problems, because it has solid mathematical foundations with which I am already familiar, and also a rigorous model of partial evaluation.
There is a pre-existing body of work on how to prove things about programs and transform and simplify them in provably correct ways in computer science: compiler theory. One of the major themes I’ve picked up from studying compilers is that different representations enable us to prove different things and perform different operations. In practice every compiler takes programs through a long series of intermediate representations. One of these representations, Static Single-Assignment (SSA) form, is strongly analogous to Pearl’s causal models. Another representation, continuation-passing style (CPS), enables a natural and precise statement of one interpretation of causal decision theory, along with a precise description of when it does and doesn’t work, such that you could prove that CDT is valid for a particular problem as a lemma and then apply CDT to it.
I haven’t proved it yet, but I think I can prove within the framework I’ve defined that Eliezer’s answer to the Prisoner’s Dilemma, “cooperate iff your opponent cooperates iff you cooperate”, is uncomputable, and that there is an infinite series of successively better approximations such that the Prisoner’s Dilemma has no optimal answer.
deleted
No one has, because CDT isn’t rigorous enough to bring into a proof framework without first disambiguating it, and there is at least one disambiguation that one-boxes and at least one disambiguation that two-boxes.
This sounds pretty cool. Are you still working on it?
“Cooperate iff your opponent cooperates iff you cooperate” is impossible if your opponent always defects. (If you defect, “your opponent cooperates iff you cooperate” is true, so you should’ve cooperated :-) Eliezer pointed that out to me a while ago.
Regarding your overall approach, choosing a specific programming language feels like a wrong step to me. At some point you will want your results to have applicability in the wider world of Turing machines and algorithms, so why not start there? It’s not fuzzy at all and people have proved a lot of rigorous stuff about Turing machines.
The linked comment seems wrong—due to fuzzy language, ironically enough. The inner iff should be testing a counterfactual, not equality. That doesn’t help with the infinite regress/computability issue, though.
Anyways, I’ve found a specific probability distribution of opponents that reads your source, checks for the presence of a sufficiently large number and makes playing PD against them reduce to the name-your-utility game. And I can transform any set of agents into a set of agents that is a Nash equilibrium, by prepending a test for whether the opponent is a member of that set, and cooperating if so.
I still don’t know whether there’s an optimal solution for PD against agents drawn from any really complex distribution like the Solomonoff prior, or against agents iteratively selected starting from the universal prior. I suspect I could construct degenerate Solomonoff-like priors that force it to have or not have an optimal solution.
I realized that yesterday when I first tried moving my examples into an actual compiler, and found that the language I’d chosen was not quite what I remembered, in ways that could be summarized as “the language is broken”. So I suspect I’m going to be making up yet another a language. I’d rather not use notation loosely, though.
If you mean I should talk about Turing machines, no way. Compare the strength of what you can prove about a program that you take through a functional representation and various augmented SSA forms, to what you can prove about Turing machines, and the difference is enormous.
If so, how do you define the truth value of that counterfactual?