Administrative
The language for this homework is:
This language is the Schlac language that we have seen in class
(#lang pl schlac
), extended with everything that we
defined in class.
The VonKoch Conjecture
In this homework you will implement a program that find a graph labeling that verifies the VonKoch conjecture (also called the RingelKotzig conjecture). This is problem 92 in NinetyNine Haskell Problems, which was adapted from NinetyNine Lisp Problems, which in turn was adapted from NinetyNine Prolog Problems. The solution that we will implement is similar in nature to the Haskell solution.
The conjecture revolves around the concept of “graceful labeling” of graphs: given a graph with N nodes, we label its nodes from 0 to N1, and each edge is labeled with the difference between the labels of the two nodes that it connects. Such a labeling is graceful if the edge labels are all unique, and a graph is said to be graceful if it is possible to find such a labeling. The conjecture is that all trees are graceful graphs. Note that a tree with N nodes has exactly N1 edges, so the conjecture actually says that we can find node labels from 0 to N1, such that the set of edge labels has all of the numbers from 1 to N1.
You will not be verifying this conjecture (that’s an open problem), but
you will write a simple function, vonkoch
, that will consume a graph,
and look for graceful labelings. The input graph will be represented as
a list of pairs, where each pair is specified using the labels of the
two nodes it connects. For example, the following tree:
 
 
6———4———2


1
is represented by the following pairs:
Note that we use numbers from 0 to N1 to specify the input graph,
but these labels are not graceful. The vonkoch
function that we
will implement will look for graceful labelings, and return a list of
solutions, each one is a list that maps input labels to a graceful label
that it found. For the above tree, this will be the first solution that
we get:
which means that this is the graceful labeling:
 
 
1———0———5


4
You can verify that the edges in this graph have differences from 1 to 6. (Note that it is easy to try your code with the graph that John is so excited with above, but Schlac is slow enough to make it impractical. After I disabled the syntactic coverage to make it run faster, I got a solution on my computer after around 2.5 hours.)
The solution will be a naive one: we will basically compute a list of all possible permutations of the 0 to N1 range, and use it as a labeling. For each such labeling, we check whether the list of resulting edge labels is unique. This test is sufficient, because if the node labels are in that range, then the differences must all be between 1 and N1 (inclusive). (The resulting program is rather slow because of the inefficient way in which we encode numerals, but it is more efficient than it looks: since the language is lazy, we never compute the full set of permutations — only those that are actually needed are actually computed. This can make some solutions in a practical lazy language (like Haskell, for example), surprisingly fast.)
Implementation
You will do this implementation in Schlac (extended with everything that we have seen in class) which means that you need to implement a lot of the “runtimesupport” for your code, but it also means that you enjoy the benefits of laziness. The main advantage here is that you don’t need to deal with the mechanics of implementing a search, you can write simpler code that simply computes all of the possible solutions, but then return only the first one — and because the language is lazy, no additional solutions are actually computed.
To make your job easier, you get a template file with holes to fill the
rest of the code in. The template file has “???
” in all holes that
you need to fill — in some cases it is just an expression in a given
definition, and in other cases the whole definition needs to be written.
For your convenience, the file contains a complete set of function
headers (contracts and purpose statements) as well as tests — so the
only thing you need to do is implement the missing code pieces. You can
(and should), of course, add tests when you think that more are needed.
Note that the tests use the conversion functions (e.g., >nat
) that
are not officially a part of Schlac, as well as using a Racket quote as
a backdoor for getting Racket values into the tests. Nontest code can
not use either of these.
Remember that this is Schlac: it is a lazy language, it is
curried, and define
cannot generate recursive definitions. Also,
many of the “library” function names resemble their Racket counterparts
— but be very careful: all values in Schlac are singleargument
functions, so you will never get any errors in Schlac code. If you
have errors in your code, they manifest themselves as errors when you
try to convert values back to Racket — and that’s if you’re lucky,
since you can also just get meaningless results. It is therefore
crucial to write correct types and to make sure that you use the values
accordingly. (The fact that you won’t get any type errors only makes
this more important.)
Work Strategy
One way to work on the various problems is to write them in the usual
course language (#lang pl
) first, and then translate the code to
Schlac. Using Typed Racket in particular is useful, since it can be
used to verify that you have the right types. This can be very helpful,
but again — you should be extremely careful with the differences
between the languages. For example, it is easy to try some code in
Racket that uses (and E₁ E₂ E₃)
, and assume that it will work the same
in Schlac — but this is wrong, since in Schlac and
is a twoargument
function, and implicit currying means that it’s the same as if you
entered ((and E₁ E₂) E₃)
which doesn’t make any sense in Schlac (but
does return a bogus result). In addition, you should remember that
since Schlac is implicitly curried when it comes to types too: a
function with a type of X Y > Z
corresponds to a Typed Racket
function with a type of (All (X Y Z) X > Y > Z)
.
You can even go with a hybrid approach: use the typed language to write the code, with some “compatibility” functions as simple stubs which have the right type but don’t really work — and the goal of this is to just make sure that you have the types right, but not for running it.
Keeping these warnings in mind, you can use the Racket template file to help you with implementing list permutations, which can be difficult on its own.
A useful approach to make your way towards a working solution is to comment out the whole code, then uncomment bits one by one as you implement the missing parts, making sure that the given tests pass, and possibly adding more tests if needed.
In some cases you might be tempted to rely on our implementation. For
example, relying on the fact that the encoding of a number n is the
“raise a function to the nth power” works only for this encoding. The
same goes for dropping if
because we implement booleans as selector
functions anyway. Doing such things is not a good idea, since it breaks
an abstraction barrier (and in the case of this language, it’s one that
cannot be enforced).
You should still define the time you spent, but you must do that within
the language, and Schlac is not really good at dealing with big numbers
(they are function compositions, so things do get slow). So, for this
homework, define hoursspent
as the (Churchencoded) number of hours
you’ve spent. There is an important point to note here — if you
define this as an expression, for example
then the actual expression will be marked as uncovered. This is because
the language is lazy, so if nothing actually uses the value of
hoursspent
the expression will be never be evaluated. In this case
you should solve this by adding a bogus test that will force evaluating
the expression, for example:
Note: If there are some parts that you cannot figure out, replace the
???
with a stub value, write a comment that you couldn’t implement the
function, and comment its tests (and, of course, apply to later
functions that depend on it, if any). For example:
;; tests  commented out since I DIDN'T IMPLEMENT IT
;; (test (>listof >nat (range 0 0)) => '())
;; ...
(test (range 0 0) => 0) ; test STUB to avoid coverage penalty