Pular para o conteúdo principal

The escape of blue eyed vampires (answer)

The island of blue eyed vampires (answer)

An initial idea

Each one needs to figure out if him/herself is blue eyed. They assume having blue eyes and see how the others react.

A technical details

There are some variations to formalize this problem using different type of logic: modal logic, temporal logic, Public Announcement Logic and so on.

I believe that those kind of prove are tedious to write and read. For now, I will write a sketch to a prove but I belive the best way to prove is using an algorimthm what basically, it would be an adaptation of DPLL algorithm (Davis–Putnam–Logemann–Loveland) that uses dedutive reasoning and prove by contraction.

Legend

\[\begin{matrix}
BlueEyed(X) :X \text{ is blue eyed.} \\
Leave(X) :X \text{ leaves.} \\
O(y) :y \text{ holds at the next (temporal) state.}
\end{matrix}\]

In this temporal simplified logic, we have a set of state that holds the in- formation of days, \(W = \{d_0, d_1, d_2, d3 \ldots , d_n\}\) and transition \(S : W \rightarrow W = \{(d_0, d_1),(d_1, d_2),(d_2, d_3), \ldots(d_{n−1}, d_n)\}\) (it means, one day is followed by the next). For any subject \(X\), \(X\) want to know if himself can leave. As soon \(X\) realize that he/she can leave he/she will leave.

Now, we want to create a “frame” with the knowledge of a specific subject in a certain point of time. But in our process, one subject will reason about what another is thinking in a recursive way (in the similar process as the minimax algorithm).

As the day follows,

\[\begin{matrix}
d_i & | & O(\phi) \\
d_{i+1} & | & \phi
\end{matrix}\]

In a frame of day \(d_i\) of subject \(X\):

\[BlueEyed(X) \Rightarrow O(Leave(X))\]

But, as the problem was announced no subject leave until \(n^{\text{th}}\) - last day: \[\begin{matrix}
\forall X, i < n, d_i \square_X & | & \neg Leave(X)
\end{matrix}\]

Two vampires example

Let us assume only two vampires: Anna and Maria. Both vampires know

\[\begin{matrix}
BlueEyed(Maria) \vee BlueEyed(Anna)
\end{matrix}\]

Now, let us examine Maria reasoning, \(\square_{\text{Maria}}\)... \[\begin{matrix}
\neg BlueEyed(Maria) & \text{(hypothesis)} \\
BlueEyed(Anna) & \text{(unit propagation)} \\
O(Leave(Anna)) & \text{(prognosis: next day Anna leaves)}
\end{matrix}\]

However, next day, Anna did not leave (what is a contradiction \(\bot\) - hypothesis is false). Therefore,

\[\begin{matrix}
\vDash BlueEyed(Maria) & \text{(law of the excluded middle)}
\end{matrix}\]

Three vampires example

Now let’s do that for 3 vampires: Anna, Maria and John.

Global knowledge

\[\begin{matrix}
BlueEyed(Maria) \vee BlueEyed(Anna) \vee BlueEyed(John) \\
BlueEyed(X) \Rightarrow O(Leave(X))
\end{matrix}\]

At, any time, there are 3 frames…: (frame 1) What Maria is thinking…(frame 2) What Maria thinks what Anna is thinking and (frame 3) What Maria thinks what Anna thinks what John is thiking.

Maria hypothesis is \(\neg BlueEyed(Maria)\). But she also KNOWS (\(\Rightarrow\) she is SURE about that) that Anna would be thinking the same way. So, if Maria hypothesis is right, for Anna, Maria would be not BlueEyed. At same time, Anna would be considering herself as not blue eyed by her own hypothesis. And, applying the same reasoning, Anna would consider what John would be thinking. And that third frame would inheritated not blue eyed for Maria and not blue eyed for Anna. Therefore, John would know that he is the only one with blue eyes and for Anna (according with Maria reasoning) the conclusion would be that John leaves next day.

However, John would not leave. So, Anna hypothesis was wrong (in frame 2). So, in frame 2, Anna concludes that she has blue eyes. But next day Anna does not leave. So Maria concludes that she must have blue eyes.

\[\begin{matrix}
& BlueEyed(Maria) ∨ BlueEyed(Anna) ∨ BlueEyed(John) \\
& BlueEyed(X) \Rightarrow O(Leave(X)) \\
d_0| & \neg BlueEyed(Maria) & \text{(Maria hypothesis)} \\
d_0| & \neg BlueEyed(Anna) & \text{(Anna hypothesis over Maria hypothesis)} \\
d_0| & BlueEyed(John) & \text{(unit propagation)} \\
d_0| & O(Leave(John)) & \text{(prognosis)}
\end{matrix}\]

The next day prognosis…\[\begin{matrix}
d_1| & Leave(John) &
\end{matrix}\]

at \(d_1\)

\[\begin{matrix}
d_1| & \neg Leave(John) \bot \\
d_1| & BlueEyed(Anna) & \text{(law of the excluded middle)} \\
d_1| & O(Leave(Anna)) & \text{(prognosis)}
\end{matrix}\]

So \[\begin{matrix}
d_2 & Leave(Anna) & \text{(prognosis)}
\end{matrix}\]

at \(d_2\)

\[\begin{matrix}
d_2|& \neg Leave(Anna) \bot \\
d_2 & \vDash BlueEyed(Maria)
\end{matrix}\]


Comentários

Postagens mais visitadas deste blog

Expressões, preconceito e racismo

Expressões preconceituosas e racistas Antes de alguma outra frase, primeiro peço licença para falar de mais um assunto do qual não domino. Falo por acreditar que um leigo presta serviço maior ao debater assunto com base em fontes (ainda que seja uma Wikipedia) e no pensamento lógico do que simplesmente se manter mudo a questões do cotidiano. Em voga agora está em falar quais são ou eram as expressões preconceituosas e racistas que até a pouco eram toleradas em muitos meios.
Como é covarde dizer que em boca fechada não entra racismo. O racismo não é perpetrado apenas por quem profere mas por quem se cala à agressão perpetrada a outrem. Mas veremos que a questão é muito mais complexa que os cães raivosos do politicamente correto querem dizer.
Tomo aqui a palavra racista, como sendo algo usado para impor a dominação de uma “raça” sobre outra. Portanto, a acusação de racismo vai muito além da mera acusação de preconceito. Não tenho o menor apreso por vitimismo barato, onde expressões que…

Um texto pós-moderno - better man

Espere olhando para as horas... são 4 horas. Tem que parar. Nesse tom melancólico, começa a modesta música "better man", uma balada pop composta por Eddie Vedder ainda na adolescência. A música é a ilustração perfeita da ironia. O próprio título é irônico, uma vez que em momento algum na música aparece um better man.

She lies and says she's in love with him, can't find a better man...

Irônico, não!? Para começar, com a personagem central da história, a mulher que aguarda tarde da noite seu esposo... Ela chega a treinar com o espelho o fim do relacionamento. E o que faz? Diz a negação do que queria dizer.

Vedder escreve músicas sobre sentimentos fortes. Sua relação com a mãe foi bastante complicada pelo o que descreve em suas canções. Na trilogia Mommy, Vedder descreve um homem perturbado com o relacionamento materno; a mãe mente para o filho sobre a identidade do pai, revela a verdade para o garoto na puberdade dizendo a ele como se parece com o verdadeiro pai e o leva …

Curry with JS

Partial application and currying with Javascript In the strict way, currying is the technique of transforming a function that takes multiple arguments (a tuple of arguments) to one function that receive only one. In such way, currying techniques allow transform one multi-parameter function in a chain of functions, each one with a single argument. Looks complicated? Blah.. it is not true.
In this little article, we are actually more interesting in partial applications. Let’s take the Mozilla Example for replace function in String. As we know, we can use a “replacer” function as paramenter for replace method in String object.
Let’s say that we want to split a String defined by a non-numerical part, a numerical part and finally a non-alphanumeric part. Here is how:
function replacer(match, p1, p2, p3, offset, string){ // p1 is nondigits, p2 digits, and p3 non-alphanumerics return [p1, p2, p3].join(' - '); }; We can try it as usual…
var newString = "abc12345#$*%".r…