"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.