Nested Quantifiers: Checking a Social Network

Click the orange Accept lab lab04 button at the top of this page and then Accept assignment. When the checklist finishes, click Open repository, and open it with the green Code button → Codespaces → Create codespace on main.

If you prefer to work on your own computer or in another editor, that is fine as well; the section Other ways to work and submit explains how.

Open data.py. The network is a dictionary that maps each person to the set of people they follow:

FOLLOWS = {
    "Ada":  {"Bora"},
    "Bora": {"Ada", "Can"},
    ...
}

So FOLLOWS["Bora"] is {"Ada", "Can"}, which means that Bora follows Ada and Can. Nobody follows themselves.

At the top of network.py you will find two small helper functions that are already written for you. follows(net, x, y) answers the question “does $x$ follow $y$?”, and people(net) gives the list of everyone in the network. You will use them in almost every task.

follows(FOLLOWS, "Bora", "Can")    # True
follows(FOLLOWS, "Can", "Bora")    # False
people(FOLLOWS)                    # ['Ada', 'Bora', 'Can', ...]

Now run the checks once, before you change anything. Every check should report that it is not implemented yet.

$ python check.py:| forall_exists: [1,2,3] with x+y=4 → True, [1,2] → False
  not implemented yet (still raises NotImplementedError)
...
0/18 checks passed

Part A asks for four general functions. Each one receives a list D (the domain) and a two-place predicate P(x, y), a function of two elements that returns True or False, such as lambda x, y: x + y == 4.

From the notes, a nested statement is a loop inside a loop, and in Python it is a call of all or any inside another one. The outer function belongs to $x$, the inner one to $y$:

# ∀x ∃y P(x, y): for every x (outer all), there is some y (inner any)
all(any(P(x, y) for y in D) for x in D)

Write forall_forall, forall_exists, exists_forall and exists_exists in the same way, choosing all or any for each position. Before you run the checks, predict the answers to these two lines and then confirm them:

forall_exists([1, 2, 3], lambda x, y: x + y == 4)   # True: 1 pairs with 3, 2 with 2, 3 with 1
exists_forall([1, 2, 3], lambda x, y: x + y == 4)   # False: no single x makes every sum equal to 4

The same predicate, the same domain, opposite answers. That is the whole message of this week.

Knowing that “everyone follows someone” is true is useful, but a program usually needs to know whom each person follows. That is what a witness is.

witnesses(D, P) returns a dictionary that gives every $x$ its first witness $y$, or None if $x$ has none. Python’s next with a default is a neat tool here: next((y for y in D if P(x, y)), None) returns the first matching $y$, or None when there is none.

witnesses([1, 2, 3], lambda x, y: x + y == 4)   # {1: 3, 2: 2, 3: 1}
witnesses([1, 2], lambda x, y: x + y == 4)      # {1: None, 2: 2}

first_failure(D, P) returns the first $x$ that has no witness at all. That $x$ is exactly the counterexample to $\forall x\, \exists y\; P(x, y)$, and it is None when the statement is true.

Now the network. In every question, “everyone” means “everyone else”, because nobody follows themselves. Each function receives the network as its parameter net, so always work with net, follows(net, …) and people(net), never with the global FOLLOWS.

Q1, everyone_follows_someone. The statement is $\forall x\, \exists y\; (x \ne y \land F(x, y))$. You can answer it in one line with your forall_exists, giving it people(net) and the predicate lambda x, y: x != y and follows(net, x, y).

Q2, celebrity. The statement is $\exists y\, \forall x\; (x \ne y \to F(x, y))$, but this time the question wants the name of the celebrity, or None. Go through every candidate $y$; a candidate is a celebrity when every other person follows them, that is, when all(x == y or follows(net, x, y) for x in P) is true. Notice how the implication $x \ne y \to F(x, y)$ became x == y or ...: an implication is false only when its hypothesis holds and its conclusion fails.

Q3, someone_follows_everyone. The mirror image of Q2: $\exists x\, \forall y\; (x \ne y \to F(x, y))$, a person whose own row is full.

$ python network.pyQ1 everyone follows someone : True
Q2 celebrity                : Ada
...

Look at data.py and check the answers by eye. Everyone except Ada follows Ada, so Ada is the celebrity. Because a celebrity exists, Q1 had to be true as well; this is the one direction that always works.

Q5, first_unreturned (do this one before Q4). Find the first pair $(x, y)$ where $x$ follows $y$ but $y$ does not follow $x$ back. Use two for loops over people(net), the outer one for $x$ and the inner one for $y$, and return the tuple (x, y) as soon as you find such a pair. If the loops finish, return None.

Q4, all_mutual. The statement $\forall x\, \forall y\; (F(x, y) \to F(y, x))$ is true exactly when Q5 finds no counterexample. That makes this a one-line function.

Q6, loners. A loner follows nobody and is followed by nobody: for every $y$, neither $F(x, y)$ nor $F(y, x)$. Return the names of all loners as a list, in the order of people(net). A list comprehension with an all(...) inside it does the job.

$ python network.pyQ4 all follows mutual       : False
Q5 first unreturned follow  : ('Bora', 'Can')
Q6 loners                   : []

From the notes, a negation moves inwards and flips every quantifier it passes:

Write not_forall_exists(D, P) as the right-hand side: call your exists_forall with a new predicate that returns the opposite of P, that is, lambda x, y: not P(x, y).

The checks compare your answer with the real negation on 60 random cases, and they also read your code. If you write not forall_exists(D, P), the value is correct but the rule is skipped, so that check will not pass.

The last part puts the specification from the notes into code.

is_sorted(b) checks $\forall i\; (b[i] \le b[i+1])$ for every position $i$ that has a next element. keeps_values(a, b) checks $\forall i\, \exists j\; (a[i] = b[j])$, which is a nested statement like the ones in Part A.

is_correct_sort(a, b) is the complete specification: $b$ must be sorted and every value must occur the same number of times in $a$ and in $b$. The notes showed why keeps_values alone is not enough, and the checks include exactly that trap:

is_correct_sort([3, 3, 1], [1, 3, 3])   # True
is_correct_sort([3, 3, 1], [1, 3, 5])   # False: a 3 was lost and a 5 appeared from nowhere

list.count(v) tells you how many times v occurs in a list. Compare the counts for every value that appears in either list.

When python check.py reports 18/18 checks passed, or when you have done as much as you can, push your work. Every push is graded out of 100.

$ git add -A$ git commit -m "Lab 4"$ git push

About two minutes later your score appears under Releases on your repository page. Your last push before Friday 23:59 is the one that counts.