tail of a functional stream
The problem was posed by John McCarthy as follows. 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:
a and b?
The following Haskell code demonstrates a generic method of encoding facts, and the knowledge about facts, and the knowledge of the knowledge, etc. Incidentally, compared to the notation in McCarthy's paper, the Haskell notation is notably concise.
Chung-chieh Shan commented: ``The basic idea is to think of a set of possible worlds. Corresponding to each person (whose knowledge is being modeled) is a partition of this set of possible worlds; each partition contains one or more worlds that this person cannot distinguish. For someone to know a fact is for all of that person's indistinguishable possible worlds to verify that fact. For Alice to know that Bob doesn't know the weather, is for all of Alice's possible worlds (relative to the real world) to reside within a Bob-partition in which the weather is not consistent across all worlds.''
Mr-S-P.lhs [4K]
Complete literate Haskell98 code
It was first mentioned in the message posted on
Lambda-the-Ultimate on Jan 27, 2003. The present version adds a
straightforward memoization.
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.
The paper discusses at great extent the history of the puzzle, its
modeling in modal `public announcement logic', and solving using
epistemic model checkers.
Anne, Bill and Cath each have a positive natural number written on their foreheads. They can only see the foreheads of others. One of the numbers is the sum of the other two. All the previous is common knowledge. The following truthful conversation takes place:What are the numbers of Bill and Cath?
- Anne: I don't know my number.
- Bill: I don't know my number.
- Cath: I don't know my number.
- Anne: I now know my number, and it is 50.
The puzzle appeared as Problem 182 in the November 2004 issue of Math Horizons.
We encode the statement of the problem as a filter on possible worlds.
The possible worlds consistent with the statement of the problem are
the solutions. `Agent A does not know
proposition phi' is interpreted as the statement that for
all worlds consistent with the propositions that A currently
knows, phi is true in some worlds but false in the others.
H.P. van Ditmarsch, W. van der Hoek, and B.P. Kooi: Dynamic Epistemic
Logic and Knowledge Puzzles
Proc. 15th International Conference on Conceptual Structures (ICCS).
LNCS 4604, pp. 45-58, Springer, 2007.
Representing knowledge about knowledge: ``Mr.S and Mr.P'' puzzle
The procedure is written in the pure functional subset of R5RS Scheme and comes with the correctness proof. We must stress that the proof was developed not after the implementation but along with the implementation. In our experience, thinking about the proof and writing it down notably helped design and code the algorithm. Once the proof was written, the code followed immediately. The code worked on the first try.
n
words within page margins, maximizing the overall neatness.
To be more precise, we wish to minimize the sum, over all lines
except the last, of the cubes of the number of blank characters at the
end of each line. See the comments in the code for more details.
The algorithm has O(n^2) time and space
complexities.
Z. Galil, K. Park:
A linear-time algorithm for concave one-dimensional dynamic programming
Information Processing Letters, v33, N6, 309-311, 1990.
David Eppstein, livejournal.com user 11011110, pointed out that
the present problem is an instance of concave 1d dynamic programming, which
admits a linear-time solution.
L
and a number N, return the set of all subsets of
L of cardinality N. Sets are represented by
lists. We will be using R5RS Scheme.
In part 1, we start with the mathematical definition of the problem, which leads to a simple, correct, but inefficient solution. We then try to systematically optimize the function until we end up with the fastest function, which is notably faster than the other solutions proposed so far. The final solution is still pure functional. We also demonstrate that the choice of the Scheme interpreter does matter in relative performance of various algorithms.
In part 2, we again start with the mathematical definition of the problem, which leads to a simple, correct, and stunningly efficient solution. The final, so far the fastest solution is still pure functional. The key was to choose the right definition.
In the discussion, Doug Quale presented lazy stream implementations in Haskell and Scheme, and compared them with the above. Eli Barzilay described various memozied versions, which have even better performance. The two USENET threads contain the excellent discussion of the relative merits of memoization and laziness, contributed by Doug Quale and Eli Barzilay. The threads also include many timing comparisons.
subsets-size-n-part2.txt [9K]
Part 2 of the article
It was originally posted as
The FASTEST subsets function [Was: Subsets of a list]
on the newsgroup comp.lang.scheme
on Sat, 12 Jan 2002 00:56:01 -0800
The article is updated with a more optimized solution, which
should perform better when compiled.
Discussion threads of the above titles, comp.lang.scheme, Jan 9-18, 2002.
primes = sieve [ 2.. ] where
sieve (p:x) = p : sieve [ n | n <- x, n `mod` p > 0 ]
is not the Eratosthenes sieve. For one thing, it uses the division
operation (or, mod). The Eratosthenes sieve specifically
avoids both division and multiplication, which were quite difficult in
old times. Mainly, as Melissa O'Neill explains below, the code
above tests every number for divisibility by all
previously found primes. In contrast, the true Eratosthenes sieve
affects only composite numbers. The prime numbers are `left out'; they
are not checked by division or numeric comparison.
Given below are several implementations of the true Eratosthenes sieve algorithm, in Scheme, Scheme macros, and Haskell. The algorithm is usually formulated in terms of marks and crossing off marks, suggesting the imperative implementation with mutable arrays. The Scheme code follows that suggestion, using two important optimizations kindly described by George Kangas.
Eratosthenes sieve, however, can be implemented purely functionally, as Scheme macros and Haskell code demonstrate. The Haskell implementation is not meant to be efficient -- rather, it is meant to be purely functional, insightful, minimalist, and generalizable to other number sieves, e.g., `lucky numbers'. Like other Haskell algorithms it produces a stream of prime numbers. The Haskell implementation stores only marks signifying the numbers, but never the numbers themselves. Not only the implementation avoids multiplication, division or the remainder operations. We also avoid general addition and number comparison. We rely exclusively on the successor, predecessor and zero comparison. The predecessor can be easily eliminated. Thus the algorithm can be used with Church and Peano numerals, or members of Elliptic rings, where zero comparison and successor take constant time but other arithmetic operations are more involved.
Eratosthenes-sieve.txt [6K]
Eratosthenes sieve and its optimal implementation
The explanation of the original Eratosthenes sieve and its
optimizations.
The original article was posted as
Re: arbitrary precision rationals
on a newsgroup comp.lang.scheme
on Tue, 13 Nov 2001 15:07:34 -0800
number-sieve.lhs [4K]
The literate Haskell98 source code for pure functional,
minimalist Eratosthenes and lucky number sieves
The code was originally posted in the article
Even better Eratosthenes sieve and lucky numbers
on the Haskell-Cafe mailing list
on Mon, 12 Feb 2007 18:37:46 -0800 (PST)
A stress test
of the syntax-rule macro-expander
Eratosthenes sieve as a syntax-rule macro, to perform
primality test of Church-Peano numerals at macro-expand time
Lucky numbers: another number sieve
<http://mathworld.wolfram.com/LuckyNumber.html>
<http://www.research.att.com/~njas/sequences/A000959>
n sequences. For example
(cross-product '((0) (0 1 2 3) (1 2)))evaluates to
((0 0 1) (0 0 2) (0 1 1) (0 1 2) (0 2 1) (0 2 2) (0 3 1) (0 3 2))The solution is especially elegant if we use the standard (SRFI-1)
append-map function.