A sort of meta-comment on modal agents: I dislike the way they are presented mathematically, in terms of logical expressions and formulas. I think it would be simpler to use some model of computation, such as the lambda calculus, and then make the agents programs instead of formulas.
For example: We first define a runtime with an evaluator, (eval exp), and then a macro (prove exp) which hands the expression to a theorem prover, and returns true if and only if the theorem prover determines that the expression will terminate and the resulting value will be true. We can also use the special form (quote exp) to quote an expression, the replacement for declaring that some parts of formulas are implicitly encoded as Gödel numbers.
An agent becomes simply a function (agent my-code opponent-code). During testing against other agents, the runtime provides the agent with its own quoted code and the opponent’s quoted code. (It’s not strictly necessary to provide the agent’s own code to itself, but doing so makes it easier to avoid having to write quines.) The runtime then evaluates both functions, to see who cooperates and who defects. Note that the agent might never terminate—which is an ambiguity that the mathematical presentation doesn’t really resolve. One way to resolve this ambiguity is to say that such is undefined behavior, and the runtime may choose cooperate or defect as it wishes.
Some examples of agents in this framework, using a Lisp-like syntax:
;; DefectBot
(define (defect-bot my-code opponent-code)
#f) ;; False stands for defection, true for cooperation
;; CliqueBot
(define (clique-bot my-code opponent-code)
(equal? my-code opponent-code))
;; FairBot
(define (fair-bot my-code opponent-code)
(prove `(,opponent-code ',opponent-code ',my-code)))
;; Payorian FairBot
(define (payorian-fair-bot my-code opponent-code)
(define (implies X Y)
(or (not X) Y))
(prove `(implies (prove `(,my-code ',my-code ',opponent-code))
(,opponent-code ',opponent-code ',my-code))))
;; JustBot
(define (just-bot my-code opponent-code)
(prove
`(,opponent-code
',opponent-code
;; Play the opponent against a copy of FairBot's code, not JustBot's code:
'(λ (my-code opponent-code)
(prove `(,opponent-code ',opponent-code ',my-code))))))
Maybe I should vibe-code this so we can have a tournament :)
You have a typo. JustBot is inserting a copy of FairBot’s code. I think, given the name JustBot, you probably meant to play the opponent against a copy of CooperateBot:
The JustBot I was copying in fact simulates against FairBot, not CooperateBot. You’re right that I did have two typos—but those were in missing quotes. I’ve now fixed it.
Also, your quotation of cooperate-bot is incorrect, because quote as a special form simply says to look at the next expression and treat it as literal data, so if an expression has already been loaded and evaluated (to give you your function cooperate-bot), you can’t get its code by just putting a quote before the symbol referring to that function. That would take some kind of environment inspection.
;; Play the opponent against a copy of 𝐂𝐨𝐨𝐩𝐞𝐫𝐚𝐭𝐞𝐁𝐨𝐭'𝐬 𝐜𝐨𝐝𝐞, not JustBot's code:
'(λ (my-code opponent-code)
(prove `(,opponent-code ',opponent-code ',my-code)))
The source of my confusion is:
You say “CooperateBot’s code” but insert Fairbot’s code.
Yes! The prover is really any function with two semantic guarantees:
If (eval exp) returns #f, so does (prove exp).
(prove exp) does not do unbounded computation, and always returns either #t or #f.
The prover does not need to be a good prover, but ideally it would be self-aware, looking for instances of prove in the expression to try to find fixed points. Note that when writing a bot, one can internally define and use their own theorem prover if they wish—and in a more barebones competition the competitor would be required to.
A sort of meta-comment on modal agents: I dislike the way they are presented mathematically, in terms of logical expressions and formulas. I think it would be simpler to use some model of computation, such as the lambda calculus, and then make the agents programs instead of formulas.
For example: We first define a runtime with an evaluator,
(eval exp), and then a macro(prove exp)which hands the expression to a theorem prover, and returns true if and only if the theorem prover determines that the expression will terminate and the resulting value will be true. We can also use the special form(quote exp)to quote an expression, the replacement for declaring that some parts of formulas are implicitly encoded as Gödel numbers.An agent becomes simply a function
(agent my-code opponent-code). During testing against other agents, the runtime provides the agent with its own quoted code and the opponent’s quoted code. (It’s not strictly necessary to provide the agent’s own code to itself, but doing so makes it easier to avoid having to write quines.) The runtime then evaluates both functions, to see who cooperates and who defects. Note that the agent might never terminate—which is an ambiguity that the mathematical presentation doesn’t really resolve. One way to resolve this ambiguity is to say that such is undefined behavior, and the runtime may choose cooperate or defect as it wishes.Some examples of agents in this framework, using a Lisp-like syntax:
Maybe I should vibe-code this so we can have a tournament :)
You have a typo. JustBot is inserting a copy of FairBot’s code. I think, given the name JustBot, you probably meant to play the opponent against a copy of CooperateBot:
The JustBot I was copying in fact simulates against FairBot, not CooperateBot. You’re right that I did have two typos—but those were in missing quotes. I’ve now fixed it.
Also, your quotation of
cooperate-botis incorrect, because quote as a special form simply says to look at the next expression and treat it as literal data, so if an expression has already been loaded and evaluated (to give you your functioncooperate-bot), you can’t get its code by just putting a quote before the symbol referring to that function. That would take some kind of environment inspection.Can you please fix your comment?
The source of my confusion is:
You say “CooperateBot’s code” but insert Fairbot’s code.
What is “just” about cooperating with FairBot?
Done! I’m not going to argue about whether it’s more just to test against FairBot or CooperateBot. I’m just copying the standard JustBot.
can the
provefunction make use of facts like’(prove X)?Yes! The prover is really any function with two semantic guarantees:
If
(eval exp)returns#f, so does(prove exp).(prove exp)does not do unbounded computation, and always returns either#tor#f.The prover does not need to be a good prover, but ideally it would be self-aware, looking for instances of
provein the expression to try to find fixed points. Note that when writing a bot, one can internally define and use their own theorem prover if they wish—and in a more barebones competition the competitor would be required to.