Solving Logic Puzzles with Dependently Typed Functional Programming

Agda is a dependently typed functional programming language and a proof assistant. Agda uses the Programs as Proof paradigm in which logical propositions are defined as types, and a proof for a given proposition is a function of the same type signature. The relationship between programs and mathematical proofs between is known as the Curry-Howard correspondence.

Dependently Typed Functional Programming

Puzzles are essentials logical propositions and solving a puzzle would involve proving that a solution is valid. Before we get into how this can be applied, let’s first understand what “logic propositions as types” and “programs as proof” mean. We also need types that represent logical reasoning. If you know a bit about Agda then you can skip to the next section.

Agda

Agda has a similar syntax to Haskell. In the following example we are defining the rules to create natural numbers. Base case, zero is a natural number. If m is natural number then it’s successor is also a natural number.

data is similar to a Haskell type-class.

For creating a function to add two natural numbers we pattern match and define each case separately. Zero plus n is n, successor of m plus n is equal to successor of m plus n (this will inductively become zero plus n).

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

one   = (suc zero)
two   = (suc one) -- or (suc (suc zero))
three = (suc two) -- or (suc (suc (suc zero)))

add : Nat → Nat → Nat
add zero    n = n
add (suc m) n = suc (add m n)

Agda has unicode support, and typically you will find most Agda code written in unicode. The same example but with unicode.

The emacs-mode for Agda comes with a convenient way to enter unicode, and a way to check how what the character is

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n = n
(suc m) + n = suc (m + n)

Equality

These are quite deep topics, please refer to the book Programming Language Foundations in Agda [2] for a more detailed explanation

An operator equality can be defined as follow. For a type A and x of type A we say that x is equal to itself. This is a reflexive relation refl .

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

With this be can create our first proof, let’s prove 1 + 2 ≡ 3. Our proof is a type correct function defined in the type 1 + 2 ≡ 3 . There can be several different functions/proof for a given proposition.

We can prove 1 + 2 ≡ 3, either with a chain of equality statements or prove it to be a reflexive relation.

proof₁ : one + two ≡ three
proof₁ =
  begin
    (suc zero) + two
  ≡⟨⟩
    (suc (zero + two))
  ≡⟨⟩
    (suc two)
  ≡⟨⟩
    (suc (suc (suc zero)))
  ≡⟨⟩
    three
  ∎

proof₂ : one + two ≡ three
proof₂ = refl

Negation

Agda relies on Intuitionistic or Constructive logic. In Intuitionistic we say that if assuming A is absurd then ¬A is valid.

-- Empty or An absurdity
data ⊥ : Set where

-- Negation
¬_ : Set → Set
¬ A = A → ⊥

A logical statement: “The glass is not empty” is intuitionistic logic means that a proof for the statement “The glass is empty” is absurd.

We can say

impossible₁ : ¬ (zero ≡ 2)
impossible₁ ()

impossible₂ : (zero ≢ 1)
impossible₂ ()

Connectives

Connectives are used to connect logical formula’s together. Given two propositions A and B, a conjuction A × B holds if both A holds and B holds. A × B is refered to as the cartesian product in set theory.

We can represent the statement “A’s cost is greater than 10 and less than 50” as

statement : (cost > 10) × (cost < 50)

Given two propositions A and B, a disjunction A ⊎ B holds if either A holds or B holds. In set theory A ⊎ B is called the disjoint union.

We can represent the statement “Either A is a knight or B is a knight” as

statement : (A ≡ knight) ⊎ (B ≡ knight)

With these we have some essentials to approach logical puzzles

Knights and Knaves

Photo by Karthik B K on Unsplash

For “Knights and Knaves” the primary information is

A very special island is inhabited only by knights and knaves. Knights always tell the truth, and knaves always lie.

First create a datatype to represent a Person. A person can be either a knight or a knave. Now, we create a function says to describe a conversation. Any proposition said by a knight is valid, any proposition said by a knave is negated.

data Person : Set where
  knight : Person
  knave  : Person

says : Person → Set → Set
says knight p = p
says knave  p = ¬ p

Note: In intuitionistic logic, a negation statement

¬ (A ≡ knight)

does not automatically mean that (A ≡ knave)

Puzzle 1

You meet two inhabitants: Zoey and Mel. Zoey tells you that Mel is a knave. Mel says, “Neither Zoey nor I are knaves.”

Puzzle Credits: https://philosophy.hku.hk/think/logic/knights.php

To start of with we can model Zoey and Mel as variable of type Person

Zoey : Person
Mel  : Person

We can represent the “Zoey tells you that Mel is a knave” as

says Zoey (Mel ≡ knave)

and the statement “Mel says, ‘Neither Zoey nor I are knaves.’ ” as a conjuction of two statements “Zoey is not a knave” and “Mel is not a knave”.

says Mel ((Zoey ≢ knave) × (Mel ≢ knave))

To form the problem statement we need to define a type that captures all the information. This is done as follows

data Solution : Set where
    soln : (Zoey : Person) → (Mel : Person) →       -- Two people Zoey Mel
      (says Zoey (Mel ≡ knave)) →                   -- Zoey's statement
      (says Mel ((Zoey ≢ knave) × (Mel ≢ knave))) → -- Mel's statement
      Solution₃

Solution

Now to solve this we need to create a function with this type

answer : Solution
answer = ?

Proof can be created interactively in Agda in Emacs. A ? create a hole, which is basically a placeholder. First let’s expand this, this using the command C-c C-r

answer : Solution
answer = soln {}1 {}2 {}3 {}4

Now we try different possibilities for Zoey and Mel and also prove Zoey and Mel’s statement. You might ask how this is different from doing this puzzle in pen and paper? The answer is the Agda’s type system ensures that your answer is correct, Agda is assisting your to prove your solution.

Agda also comes with an auto proof search utility, entering C-c C-a in a hole tries to automatically find a proof. Let try seeing if Agda can find a proof from hole 3 (statement “Zoey tells you that Mel is a knave”)

answer : Solution
answer = soln₃ knight knave refl {}4

Agda automatically filled in that Zoey is a knight and Mel is a knave. As a knight Zoey is telling the truth, the proof is that it is a simple reflexive relation.

Proving Mel’s statement is a bit different because it involves negation. Mel says “Neither Zoey nor I are knaves”, we need to prove that at-least one of these statements is absurd.

We define a property called ¬-elim to eliminate absurd statements. ¬-elim means, “If you have a statement that a glass is not empty ¬-x and a statement that the glass is empty x, then the existence of both the statement together in absurd”. So how does this property apply for us?

In our case when Mel is knave, Mel’s statement implies that “Zoey a knight not a knave” and “Mel a knave is not a knave”. “A Knave is a Knave” is established by a reflexive relation. The existance of the second statement “Mel a knave is not a knave”, when reflexive relation is established is absurd by our property ¬-elim. QED Mel’s statement is negated.

¬-elim : {A : Set} → ¬ A → A → ⊥
¬-elim ¬x x = ¬x x

answer : Solution
answer = soln knight knave
  refl
  λ{ ⟨ knv≢kni , knv≢knv ⟩ → ¬-elim knv≢knv refl}

This can be compiled with C-c C-l , Agda’s typechecker validates it indicating that the solution to our Puzzle is that Zoey is a Knight and Mel is a Knave.

Puzzle 2

You meet two inhabitants: Peggy and Zippy. Peggy tells you that “of Zippy and I, exactly one is a knight’. Zippy tells you that only a knave would say that Peggy is a knave.

Puzzle Credits: https://philosophy.hku.hk/think/logic/knights.php

Let’s look at the second statement “Zippy tells you that only a knave would say that Peggy is a knave”. n this case Zippy is statement is nested, we be modelled as a nested say

(says Zippy (says knave (Peggy ≡ knave)))

The first statement “of Zippy and I, exactly one is a knight”, can be said as “Either “zippy is a knight and peggy is not a knight” or “zippy is not a knight and peggy is a knight””. The “either-or” is a disjoint union, the “and” is a cartesian product. So together it can be said

(Zippy ≡ knight × Peggy ≢ knight) ⊎ (Zippy ≢ knight × Peggy ≡ knight)

Model

The final model for this puzzle can be given as

data Solution₂ : Set where
  soln₂ : (Peggy : Person) → (Zippy : Person)
    → (says Peggy ((Zippy ≡ knight × Peggy ≢ knight) ⊎ (Zippy ≢ knight × Peggy ≡ knight)))
    → (says Zippy (says knave (Peggy ≡ knave)))
    → Solution₂

I wasn’t able to use the auto solver in this case, but I was able to validate my hypothesis with Agda.

Possibility 1:

Assuming Zippy is a knight, the second statement “Zippy tells you that only a knave would say that Peggy is a knave”, implied that Peggy should be knight. Using auto-complete on the second statement, Agda auto-fills a proof and that Peggy is a knight. However the first statement cannot be satisfied as it says that only one of them is a knight, hence Zippy is a knave.

possibility₁ : Solution₄
possibility₁ = soln₄ knight knight
  {!!}
  λ ()

Possibility 2:

Using what we learnt Zippy is knave, we can auto-search for a proof for the first statement, this gives us that Peggy is a knight. This cannot satisfy the second statement as it would mean that Zippy is telling the truth that a knave will lie that Peggy is a knave. Hence Peggy is also a knave.

possibility₂ : Solution₄
possibility₂ = soln₄ knight knave
  (inj₂ ⟨ (λ ()) , refl ⟩)
  {!!}

Answer:

If we assume that both Peggy and Zippy are knave, then we can prove the both the statements are absurd. None of them are knights so the first statement is absurd. Zippy’s statement is absurd as “it is absurd for a knave to say the truth that Peggy is a knave”. QED Peggy is a knave and Zippy is a knave.

answer₂ : Solution₂
answer₂ = soln₂ knave knave
  (λ{ (inj₁ ()) ; (inj₂ ())})
  (λ knv≢knv → ¬-elim knv≢knv refl)

Why is this one complex?

Solving the second puzzle where both people where knaves was more difficult compared to the first one. And at first sight it might look as if we are just considering both the statements to be absurd without constructing from a known valid proposition.

In the second puzzle the second statements’ proof is case of inverse of double negation. In intuitional logic double negation is not provable but the inverse of it is provable. The valid statement that a “knave ≡ knave” implies that the double negation of the statement is valid.

-- Not provable in intuitional logic
postulate
  ¬¬-elim : {A : Set} → ¬ ¬ A → A

¬¬-intro : ∀ {A : Set} → A → ¬ ¬ A
¬¬-intro x  =  λ{¬x → ¬x x}

answer₃ : Solution₂
answer₃ = soln₂ knave knave
  (λ{ (inj₁ ()) ; (inj₂ ())})
  (¬¬-intro refl)

Conclusion

In this article we say a very brief introduction to the dependently typed functional programming language Agda. We looked at an example of how to represent the “knights and knaves” puzzle’s statements/propositions as types and how to prove a solution.

If you are interested to know more about this topic or which to see other example, let me know in the comments.

References

1. https://agda.readthedocs.io/en/latest/getting-started/a-taste-of-agda.html
2. Wadler, Philip, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Available at https://plfa.inf.ed.ac.uk/22.08/. 2022.
3. Proposition as Types, Numberphile, https://www.youtube.com/watch?v=SknxggwRPzU
4. Proposition as Types, Wadler, https://www.youtube.com/watch?v=IOiZatlZtGU
5. https://pwparchive.wordpress.com/2012/09/06/logical-puzzles-in-agda/
6. https://math.stackexchange.com/questions/2400914/why-do-i-keep-running-into-contradictions-in-this-problem-knights-and-knaves-va

Disclaimer: The statements and opinions expressed in this blog are those of the author(s) and do not necessarily reflect the positions of Thoughtworks.