Thue Sequences, Lambda Calculus Circular Program

home1 home2
and the


also see:

Thue sequences, after Axel Thue, are sequences over an alphabet of three {1,2,3} such that no subsequence is immediately repeated. e.g. 1213121 is a Thue sequence that cannot be extended 12131211  ×,  12131212  ×,  12131213  ×. However, there are Thue sequences of any length. (There are no solutions longer than 3 for binary sequences, and finding solutions is easier for alphabets larger than three.)

The ``circular program'' below builds a tree of Thue sequences. Note that within function `build', the tree data-structure `T' and functions `toplevel' and `f' are mutually recursive. The program relies on the fact that a partial soln `abcde' can be extended with `f' iff its shadow, `bcdef', is already in tree at the previous level; this avoids repeating many tests on constraints that have already been treated at a higher level. The subtree for `abcde' is the subtree of `bcde' less any `a' nodes. The tree of all solutions is notionally infinite, but the program prints one branch to a finite depth so only a finite part of the tree is evaluated thanks to lazy evaluation.

See L. Allison. Applications of Recursively Defined Data Structures. Australian Computer Journal 25(1) pp14-20, Feb 1993.

let rec
 even = lambda n. (n/2)*2=n,

 repeated = lambda len. lambda s.
   { test:  ? s = s2;s2 ? }
   let rec
     r = lambda half. lambda s2.
       if half=len/2 then
         let rec
           r2 = lambda s1. lambda s2.
             if null s2 then true
             else if hd s1=hd s2 then
               r2  tl s1  tl s2
             else false
         in r2 s  tl s2
       else r (half+1) tl s2
   in r 1 s,

 paths = lambda depth. lambda T.
   {paths from root of T to a given depth}
   let rec
     across = lambda d. lambda Ancestors.
              lambda T. lambda Rest.
       if null T then Rest
       else down d (hd T :: Ancestors) (hd tl T)
                   (across d Ancestors tl tl T Rest),
     down = lambda d. lambda Ancestors.
            lambda T. lambda Rest.
       if d >= depth then Ancestors :: Rest
       else {d < depth} across (d+1) Ancestors T Rest
   in across 1 nil T nil

in let                        { build does the work }
 build = lambda N.
   let rec
     T = toplevel 1,

     toplevel = lambda M.
       if M > N then nil
       else M :: ((f 2 (M::nil) T) ::
                  (toplevel (M+1))),

     f = lambda len. lambda seq. lambda Shadow.
       if null Shadow then nil
         others = f  len seq  tl tl Shadow,
         seq2 = hd Shadow :: seq
       in if even len and repeated len seq2 then others
          else (hd Shadow) ::
               ((f (len+1) seq2  hd tl Shadow)::others)
   in T

in hd( paths 20 ( build 3 ))  {print one}

{\fB Tree of Thue Sequences. \fP}

{see: L. Allison,
      Applications of Recursively Defined Data Structures.
      Australian Computer Journal 25(1) 14-20 Feb 1993
tree == list of (elt x subtree)
NB. `T' is a self-referential data structure
    i.e. a circular program.

123  note that a partial soln `abcde'
 32  can be extended with f iff
213  its shadow, `bcdef', is already
 31  in tree at previous level.  The subtree
312  for abcde is the subtree of bcde
 21  less any `a' nodes.

Also see:

Coding Ockham's Razor, L. Allison, Springer

A Practical Introduction to Denotational Semantics, L. Allison, CUP

free op. sys.
free office suite
~ free photoshop
web browser

λ ...
:: list cons
nil the [ ] list
null  predicate
hd head (1st)
tl tail (rest)

© L. Allison   (or as otherwise indicated),
Faculty of Information Technology (Clayton), Monash University, Australia 3800 (6/'05 was School of Computer Science and Software Engineering, Fac. Info. Tech., Monash University,
was Department of Computer Science, Fac. Comp. & Info. Tech., '89 was Department of Computer Science, Fac. Sci., '68-'71 was Department of Information Science, Fac. Sci.)
Created with "vi (Linux + Solaris)",  charset=iso-8859-1,  fetched Thursday, 20-Jun-2024 16:32:58 AEST.