10
$\begingroup$

How can we define in a proof assistant (eg., Coq) a notion of a 2-player game, where each player is a program that has access to the opponent's source code?

Background: In Open Source Game Theory, we think about bots that reason about each other (prove theorems), knowing the other's source code. I would like implement such bots in a proof assistant, if possible. (https://arxiv.org/pdf/2208.07006.pdf, Open Problem 4)

What I have in mind would looks like this:

Inductive outcome := Cooperate | Defect.
(*  Dupoc is short for Defect Unless Proof of Cooperation   *)
Definition Dupoc (n:N) (bot2 : N -> bot -> outcome) : N -> bot -> outcome :=
    'try for n steps to find a proof that bot2 n self = Cooperate, if found':
        return Cooperate
    else
        return Defect.

The point is that we want to run the agents together with each other as input:

Definition game n1 bot1 n2 bot2 := (bot1 n1 bot2, bo2 n2 bo1).

Of course, the type bot does not exist as I have written it. Is there a way to actually make this happen?

The other problem is that the bot's function is trying to find a proof and returning a bool that reflects the success. Is this possible in some proof assistant? The proof assistant would have to have access to its own inner workings somehow, which seems hard.

I think I could solve the problem by having a Coq implementation in Coq.

Then I could have, like in the paper:

Inductive CoqTokens := ...
Definition BotExpression := ... (* A valid expression for a Bot *)
Class Bot := {
    play : BotExpression -> outcome,
    source : BotExpression (* This should be the source code for 'play' in our Coq-in-Coq implementation *)
}.
Definition game bot1 bot2 := (bot1.play bot2.source, bot2.play bot1.source).

But this seems very much work if it is possible. The Coq implementation in Coq still needs to contain everything about proofing. And I am not sure if it actually solves the problem.

$\endgroup$
15
  • 1
    $\begingroup$ I’m having trouble finding your question. $\endgroup$
    – Jason Rute
    Oct 11, 2022 at 11:27
  • 1
    $\begingroup$ If I understand correctly, your question is something like “how can we define in a proof assistant (eg. Coq) a notion of game, where each player in the game has access to the other's code ?”. Is this correct? $\endgroup$ Oct 11, 2022 at 12:14
  • 1
    $\begingroup$ Why do the bots "need" to prove anything? They just need to compute their moves, right? Could you give a scenario where it is important for a bot to actually produce a proof? $\endgroup$ Oct 11, 2022 at 21:49
  • 3
    $\begingroup$ One difficulty here is one of meta vs object level (or, as computer scientist call it, shallow vs deep embedding): both your bots and the proofs they manipulate can be either Coq functions/proofs or representation of code/proofs inside Coq. You seem to want to use the first, even if this means you have to deal with some form of quotation. Indeed, this lets you use all the power of Coq to define your bots, but it is unclear to me that this is something you need or want. Having a poorer language for bot definition and proofs would make it much easier to reason on them. $\endgroup$ Oct 12, 2022 at 13:45
  • 2
    $\begingroup$ A really cooperative robot would provide a proof that it is cooperative. Checking that a proof is valid is a lot easier than finding it. $\endgroup$ Oct 12, 2022 at 15:24

2 Answers 2

9
$\begingroup$

As you found out, the usual technique to solve this kind of difficulty is to introduce a notion of "code" (what you called BotExpression), which expresses the behaviour of your bot. Once you are happy with your codes, you can in a second time define a "decoding" function, something which takes in a code and spits out the expression, but this time as an actual Coq function. Taking the notations from your question, this means that you should be able to define a function that takes in source and outputs play. Note that to do this you do not have to reify all the syntax of Coq. Indeed, the actions available for your bots can probably be defined with a set of primitives smaller than full-fledged Coq. This lets you avoid the problem of using some form of self-description of the meta-language (which are very complicated beasts).

Similarly, you might also want to have such an encoding for proofs, again because your bots need to manipulate "concrete" data rather than meta-proofs in the ambient theory. Regarding formalization of logic, and also to give you ideas on the general code/decoding setting, you might want to give a look at eg. this library formalizing first-order logic.

Finally, there is a second issue you might stumble upon, either in the definition of your decoding function, or that of a play, which is related to the definition of functions in Coq. Indeed, as Coq lets you only define total/terminating functions, quite a lot of things with a "self-recursive" flavour are not definable as functions, as they would lead to non-terminating behaviour. In such a case, a standard solution is to replace the type A -> B by the type A -> B -> Prop, ie. replace an actual function by its graph. This avoids termination issues, and also determinism: since you do not encode a game as a function, you can have multiple choices to move on. Moreover, if you define your relation as an inductive one, you can reason by induction on it, which is probably the kind of reasoning principles you will be after.

$\endgroup$
2
$\begingroup$

Here is a theoretical way you could do this in Lean 4. The key is that you can prove stuff about pure code in Lean. Lean's Declaration and Expr datatypes are pure code I believe, so a lot of work is done for you. Type checking, however, while implemented in Lean 4, is not pure (or I don't think it is), so you would have to write a pure type checker. Automation would also be a lot of work.

import Lean

inductive Outcome
| Cooperate
| Defect

-- A bot is a pure Lean fuction which takes in it's
-- own declaration and that of its opponent to produce an Outcome.
def Bot := Lean.Declaration -> Lean.Declaration -> Outcome

-- Pure code to run the game
def runGame (bot1 bot2 : Bot) (bot1Decl bot2Decl : Lean.Declaration) : Outcome × Outcome :=
  (bot1 bot1Decl bot2Decl, bot2 bot2Decl bot1Decl)

-- -----------------
-- Code needed to build the bots

-- Pure code for checking that a proof expr has the desired type expression.
-- Since type checking in Lean is undecidable, we add a timeout.
-- This code doesn't currently exist in this pure form but it could.
-- Just rewrite enough of the Lean kernel code using pure code and a timeout.
def checkProof (proof : Expr) (expectedType : Expr) (timeout : Nat) : Bool := sorry

-- Pure code for generating the expression
-- `selfBot selfDecl otherDecl = Outcome.Cooperate`
--I don't think this would be hard to write in a pure form.
def cooperateExpr (selfBotDecl otherDecl : Lean.Declaration) : Expr := sorry

-- My cooperate bot
def coorperateBot (selfBotDecl otherDecl : Lean.Declaration) : Outcome := Outcome.Cooperate

-- My bot which sees if the opponent is a simple coorperate bot
def checkIfOpponentIsCooperateBot (selfBotDecl otherBotDecl : Lean.Declaration) : Outcome :=
  -- the thing I'm trying to prove, namely `otherBot otherBotDecl selfBotDecl = Outcome.Cooperate`
  let oppCoopExpr : Lean.Expr := cooperateExpr otherBotDecl selfBotDecl
  -- try the simplest proof, namely `rfl`
  let proof : Lean.Expr := Lean.reflExpr oppCoorExpr  -- not correct code but this can be done
  -- check if proof is valid
  if checkProof proof oppCoopExpr 100 then
    Outcome.Cooperate
  else
    Outcome.Defect

-- Build more complicated bots by extending the logic for
-- `let proof : Expr := ...`
-- one could even implement search procedures
-- however almost all of Lean's automation isn't pure code,
-- so one would have to rewrite it to be pure I believe


-- --------
-- Running the game with the IO monad

-- Unpure meta code to look up the bots declarations and run the game
def runGameIO (bot1 bot2 : Bot) (bot1Name bot2Name : String) : IO (Outcome × Outcome) := do
  let bot1Decl <- Lean.get_decl bot1Name  -- not correct code but this can be done
  let bot2Decl <- Lean.get_decl bot2Name  -- not correct code but this can be done
  return (runGame bot1 bot2 bot1Decl bot2Decl)

def Outcome.repr : Outcome -> String
| Cooperate => "Cooperate"
| Defect => "Defect"

def main : IO Unit := do
  -- run game
  let result <- runGameIO
    coorperateBot checkIfOpponentIsCooperateBot
    "coorperateBot" "checkIfOpponentIsCooperateBot"
  -- print result
  IO.println result.1.repr
  IO.println result.2.repr
```
$\endgroup$
3
  • $\begingroup$ Can you give me a resource where I can learn or infer how to write the pure type checker? E.g. It would be useful to have the unpure type checking implemented in Lean. I can't seem to find it in the GitHub repo. $\endgroup$ Oct 12, 2022 at 15:31
  • $\begingroup$ @MatthiasGeorgMayer Sorry for the late answer. I looked into it more and the Lean kernel code seems to be in Lean.Meta.Basic however, I think that a lot of the kernel is still written in C++. Also, you can look at external checkers written in Haskell (github.com/leanprover/tc) and github.com/gebner/trepplein (Scala) for Lean 3. They haven't yet been translated to Lean 4. $\endgroup$
    – Jason Rute
    Oct 19, 2022 at 17:34
  • $\begingroup$ I'll try to flesh out my answer more this weekend if I have time. In particular, I think there are a few smaller considerations I didn't think though in my original answer. $\endgroup$
    – Jason Rute
    Oct 19, 2022 at 17:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.