=======================================
REDUCERON MEMO 47
Descriptions of several F-lite programs
Colin R, Matthew N
4 May 2010
=======================================
Line counts are for F-lite sources including all required auxiliary
functions.
Adjoxo (106 lines)
An adjudicator for the game noughts and crosses, aka. tic-tac-toe.
The input is a game position, and the output is one of the three
values Win, Draw or Loss indicating the outcome with best play for
each of the players whose turn it might be. The method is the usual
minimax recursive evaluation of completed game trees.
Braun (51 lines)
A Braun tree is a balanced binary tree offering an efficient yet
simple implementation of flexible arrays. The program tests the
property that converting a list to a Braun tree and back again is
equivalent to the identity function.
Cichelli (200 lines)
Finds a perfect hash function for Haskell keywords. It uses a
backtracking search to find an assignment of natural-number values to
each letter that starts or ends a keyword such that hash values for
keywords, computed as start-value + end-value + length, are unique and
occupy a small integer range without gaps.
Clausify (131 lines)
Puts propositional formulae in clausal form using a multi-stage
transformation of formula-trees. Almost a purely symbolic application,
with hardly any arithmetic.
Fib (10 lines)
Computes the Nth number in the fibonacci sequence using a simple but
naive doubly-recursive function definition. A purely arithmetic
program involving no data structures at all.
Knuthbendix (533 lines)
The Knuth-Bendix completion method tries to derive a convergent
term-rewriting system for a given equational theory and
symbol-weighting scheme. It is a typical symbolic computing
application from computer algebra. The example input used in the
program gives group-theoretic axioms from which ten rewriting rules
are derived.
Mate (393 lines)
Solves chess end-game problems of the form "P to move and mate in N".
The method is brute-force search in an explicit AND-OR game tree
developing the given position to depth 2N-1. Boards are represented
by a square-piece assocation list for each player, where squares are
coded as rank-file numeric pairs, so there is a fair amount of
primitive arithmetic and comparison.
MSS (47 lines)
Computes the maximum segment sum of a list of integers. Works by
dividing the input list into all sub-lists, computing the sum of each,
and returning the maximum.
OrdList (46 lines)
Checks the property that insertion of a number into an ordered list of
numbers results in a list that is still ordered. Numbers are
represented as peano numerals, so this is a purely symbolic program.
Parts (54 lines)
Computes a celebrated number-theoretic function, the number of
partitions of n, where a partition is a bag of positive integers that
sum to n. There is a sophisticated closed formula for this number,
but the method here is to list and count partitions explicitly.
PermSort (39 lines)
Enumerates the permutations of a list of numbers, and returns the
first ordered permutation.
Queens (47 lines)
Solves a programming problem made famous by Wirth: place N queens on
an NxN chess board so that no two of queens occupy a common rank, file
or diagonal. The solution involves backtracking, list processing and
an inner recursive loop that testing the safety of each candidate
position for a new queen by primitive arithmetic comparisons with the
coded positions of queens already in place.
Queens2 (62 lines)
A purely symbolic solution to the N-queens problem. Represents the
board as a list of lists. Places a queen on one row at a time,
maintaining a grid of threatened squares, and backtracks if a queen
cannot be placed.
Sudoku (209 lines)
A Sudoku solver due to Richard Bird. Fills the blank cells on a
Sudoku board with valid digits, pruning many possible choices that
cannot possibly lead to a solution.
Taut (95 lines)
A tautology checking program based on an example from Hutton's book.
The method is a brute-force evaluation for all possible boolean
assignments to variables.
While (96 lines)
A structural operational semantics of Nielson and Nielson's While
language applied to a program that computes the number of divisors of
given integer.