Solving the "Mr.S and Mr.P" puzzle by John McCarthy: Formalization of two Puzzles Involving Knowledge McCarthy, John (1987). http://www-formal.stanford.edu/jmc/puzzles.html We pick two numbers a and b, so that a>=b and both numbers are within the range [2,99]. We give Mr.P the product a*b and give Mr.S the sum a+b. The following dialog takes place: Mr.P: I don't know the numbers Mr.S: I knew you didn't know. I don't know either. Mr.P: Now I know the numbers Mr.S: Now I know them too Can we find the numbers a and b? The following is a literate Haskell code. It can be loaded as it is in Hugs or GHCi. It takes a while to compute; the optimizations are straightforward; yet we deliberately chose the simplest code. A compiled version should be faster. Chung-chieh Shan has pointed out the paper Hans P. van Ditmarsch, Ji Ruan and Rineke Verbrugge Sum and Product in Dynamic Epistemic Logic Journal of Logic and Computation, 2008, v18, N4, pp.563--588. that discusses at great extent the history of the riddle, its modeling in modal `public announcement logic', and solving using epistemic model checkers. > module MrSP where First, let's define good numbers > good_nums = [2..99]::[Int] Given a number p, find all good factors a and b (a>=b) and return them (the pairs of them) in a list. We use the obvious and straightforward memoization (tabling): > good_factors_table = map gf [0..] > where > gf p = [ (a,b) | a<-good_nums, b<-good_nums, a >= b, a*b==p ] > good_factors p = good_factors_table !! p Given a number s, find all good summands a and b (a>=b) and return the pairs of them in a list > good_summands_table = map gs [0..] > where > gs s = [ (a,b) | a<-good_nums, b<-good_nums, a >= b, a+b==s ] > good_summands s = good_summands_table !! s > -- Test if a list is a singleton > singleton_p [_] = True > singleton_p _ = False Let's encode the first fact: Mr.P doesn't know the numbers. Mr. P would have known the numbers if the product had had a unique good factorization > fact1 (a,b) = not (singleton_p \$ good_factors \$ a*b) Let's encode the second fact: Mr.S doesn't know the numbers > fact2 (a,b) = not (singleton_p \$ good_summands \$ a+b) Let's encode the third fact: Mr.S knows that Mr.P doesn't know the numbers. In other words, for all possible summands that make a+b, Mr.P cannot be certain of the numbers > fact3 (a,b) = all fact1 (good_summands \$ a+b) Let's encode the fourth fact: Mr.P _now_ knows that fact3 is true and is able to find the numbers. That is, of all factorizations of a*b there exists only one that makes fact3 being true. > fact4 (a,b) = singleton_p \$ filter fact3 (good_factors \$ a*b) The fifth fact is that Mr.S. knows that Mr.P found the numbers: of all the possible decompositions of a+b, there exists only one that makes fact4 true. > fact5 (a,b) = singleton_p \$ filter fact4 (good_summands \$ a+b) Finally, we compute the list of all numbers such that fact1..fact5 hold: > result = [(a,b) | a<-good_nums, b<-good_nums, a >= b, > all (\$ (a,b)) [fact1,fact2,fact3,fact4,fact5] ] The answer is *Main> result [(13,4)] That is, a unique answer. Note how Haskell notation is concise, compared to the one employed in the paper by McCarthy.