head	1.1;
access;
symbols;
locks; strict;
comment	@# @;


1.1
date	92.06.18.17.42.03;	author ids;	state Exp;
branches;
next	;


desc
@@


1.1
log
@Initial revision
@
text
@%export surreal sign
        less_than greater_than equals lesseq greateq diff
        plus negative minus times reciprocal divided_by ordinal_sum
        over num_to_surreal ns surreal_to_num sn
        create_surreal sign_expansion

|| SIGN-EXPANSION-BASED IMPLEMENTATION OF THE SURREALS

|| This package implements the surreals (not general games)
|| using streams of signs, each either '+' or '-', and
|| lazy evaluation as the execution method. The streams can
|| either be finite or of length w.





|| ABSTRACT TYPE DECLARATIONS

|| the basic type surreal

abstype surreal
with

     || the basic operations

     || comparison operations

     less_than :: surreal -> surreal -> bool
     greater_than :: surreal -> surreal -> bool
     equals :: surreal -> surreal -> bool
     greateq :: surreal -> surreal -> bool
     lesseq :: surreal -> surreal -> bool
     diff :: surreal -> surreal -> bool

     || arithmetical operations

     plus :: surreal -> surreal -> surreal
     negative :: surreal -> surreal
     minus :: surreal -> surreal -> surreal
     times :: surreal -> surreal -> surreal

     reciprocal :: surreal -> surreal
       || WARNING: input must be a dyadic rational

     divided_by :: surreal -> surreal -> surreal
       || WARNING: denominator must be a dyadic rational

     ordinal_sum :: surreal -> surreal -> surreal


     || conversion facilities

     || conversion between surreals and Miranda system numbers

     over :: num -> num -> surreal
     num_to_surreal :: num -> surreal
       ns :: num -> surreal || abbreviation for num_to_surreal
     surreal_to_num :: surreal -> num
       sn :: surreal -> num || abbreviation for surreal_to_num

     || conversion between surreals and explicit lists of signs

     create_surreal :: [sign] -> surreal
     sign_expansion :: surreal -> [sign]


     || print-representation for type surreal

     showsurreal :: surreal -> [char]







|| CONCRETE TYPE DECLARATIONS

|| useful type synonym "sign" for {'+', '-'}
|| Note: Miranda can only express this as "char".

sign              == char
|| sign           == '+' | '-'

|| concrete representation of surreal---a stream of signs

surreal           == rep_surreal
rep_surreal       == [sign]

|| associated declarations, for internal purposes

bitstream         == [symbolic_bit]
|| used especially in multiplication
symbolic_bit      == char
|| symbolic_bit == '0' | '+' .....for binary streams

twisted_surreal   == [twisted_sign]
|| used especially in addition
twisted_sign      == char
|| twisted_sign == '+' | '0' | '-'

twisted_bitstream == [twisted_bit]
|| used occasionally in multiplication routines
twisted_bit       == char
|| twisted_bit == '0' | '+' | '2' ['2'=overflow]







|| IMPLEMENTATION OF USER-LEVEL FUNCTIONS

|| These functions are essentially the repertoire of
|| arithmetical operators and comparison operators,
|| plus some conversion facilities between surreals
|| and Miranda system numbers and between surreals
|| and sign-expansions.

|| the basic operations

|| comparison operations

|| less_than :: surreal -> surreal -> bool
|| for sign-expansions, "less_than" involves simply
|| checking their lexicographical ordering, under the
|| convention '-' < blank < '+'.
  []      $less_than []      = False
  []      $less_than ('-':y) = False
  []      $less_than ('+':y) = True
  ('-':x) $less_than []      = True
  ('-':x) $less_than ('-':y) = x $less_than y
  ('-':x) $less_than ('+':y) = True
  ('+':x) $less_than []      = False
  ('+':x) $less_than ('-':y) = False
  ('+':x) $less_than ('+':y) = x $less_than y

|| greater_than :: surreal -> surreal -> bool
|| swapped version of "less_than"
  x $greater_than y = y $less_than x

|| equals :: surreal -> surreal -> bool
|| sign-expansions have a huge advantage over the explicit
|| set-based version: equality is simply syntactic 
|| identity, ie, the system's "=" will suffice
  equals = =

|| greateq :: surreal -> surreal -> bool
|| greater than or equal to
  x $greateq y = ~(x $less_than y)

|| lesseq :: surreal -> surreal -> bool
|| less than or equal to
  x $lesseq y = ~(x $greater_than y)

|| diff :: surreal -> surreal -> bool
|| different from; as with equality, the system's own 
|| operator suffices for sign-expansions
  diff = ~=

|| arithmetical operations

|| plus :: surreal -> surreal -> surreal
|| implemented using the binary stream interpretation of
|| sign-expansions. Support functions appear later.
  x $plus y = tidyup (x $naive_plus y)

|| negative :: surreal -> surreal
|| negation is extremely simple with sign-expansions: all
|| pluses become minuses and vice versa.
  negative = map opposite

|| minus :: surreal -> surreal -> surreal
  x $minus y = x $plus negative y

|| times :: surreal -> surreal -> surreal
|| the most complex of the operators to be implemented, and
|| also that with the most thorny theoretical problems.
|| See main body of report for full discussion.

  || special cases of multiplication by zero or one
  [] $times y = []
  x $times [] = []
  "+" $times y = y
  x $times "+" = x

  || convert negative numbers to positive for uniformity
  ('-':x) $times y = negative (negative ('-':x) $times y)
  x $times ('-':y) = negative (x $times negative ('-':y))

  || from here on down, both x and y begin with '+', and can
  || be passed to the auxiliary function "intfractimes".
  x $times y = intfractimes (intfrac x) (intfrac y) 0 0

|| reciprocal :: surreal -> surreal
|| WARNING: input must be a dyadic rational
|| This is an incomplete version, included for the sake of
|| making some reciprocals and divisions possible.
  reciprocal [] = error "Can't divide by zero!"
  reciprocal ('-':rest) = negative 
                          (reciprocal (negative ('-':rest)))
  reciprocal ('+':rest) = get_reciprocal 0 1 ('+':rest)

|| divided_by :: surreal -> surreal -> surreal
|| WARNING: denominator must be a dyadic rational
  x $divided_by y = x $times reciprocal y

|| ordinal_sum :: surreal -> surreal -> surreal
|| Yet another case when changing to sign-expansions gives
|| enormous simplifications in the algorithm. It turns out 
|| the ordinal sum of two sign-expansions is just their
|| concatenation end-to-end!
  ordinal_sum = ++


|| conversion facilities

|| conversion between surreals and Miranda system numbers

|| over :: num -> num -> surreal
|| given two numbers, returns their ratio as a surreal,
|| infinite if necessary
|| eg, 2 $over 3 = "+-+-+-+-+-+-+-+-+-+-+-+-+-......."
  x $over y = error "over: division by zero attempted", y=0
            = (-x) $over (-y), y<0
            = negative ((-x) $over y), x<0
            = '+':((x-y) $over y), x>=y
            = normalize (x $naive_over y), otherwise

|| num_to_surreal :: num -> surreal
|| converts a Miranda system number into the corresponding surreal
  num_to_surreal n = n $over 1

|| ns :: num -> surreal
|| abbreviation for num_to_surreal
  ns = num_to_surreal

|| surreal_to_num :: surreal -> num
|| converts a surreal into the corresponding Miranda system number
  surreal_to_num [] = 0
  surreal_to_num ('-':rest) = -(surreal_to_num (negative ('-':rest)))
  surreal_to_num ('+':rest) 
    = limiting_value (approximation_stream 0 1 ('+':rest))

|| sn :: surreal -> num
|| abbreviation for surreal_to_num 
  sn = surreal_to_num 

|| conversion between surreals and explicit lists of signs

|| create_surreal :: [sign] -> surreal
|| creates a surreal from its sign-expansion
  create_surreal = id

|| sign_expansion :: surreal -> [sign]
|| converts a surreal into its sign-expansion
  sign_expansion = id









|| SUPPORTING AND AUXILIARY FUNCTIONS TO BACK UP
|| THE USER-LEVEL FUNCTIONS

|| In this section are the nitty-gritty details of the
|| package. The supporting functions perform the analysis of
|| sign-expansions into their binary interpretations, split
|| them into integer and fractional parts, and so on. 

|| They then carry out equivalent binary operations in ways
|| specially constructed for lazy evaluation, with the
|| "state" of knowledge about the answer stream manipulated 
|| in a buffer and output only when it's known to be
|| unchangeable by the summed effects of all future impacts
|| ---and never before.

|| This is the general principle behind all the routines that
|| depend critically on lazy evaluation. In fact it's a
|| principle to be used in any lazy-evaluation work, not
|| just the surreals.

|| supporting operations for addition

naive_plus :: rep_surreal -> rep_surreal
                -> (rep_surreal, twisted_surreal)
|| adds two surreals producing an "untidy" answer stream
|| consisting of an integer part and a twisted fractional
|| part (ie, a fractional part that may contain zeroes as
|| well as pluses and minuses). This is then passed to
|| "tidyup", which converts the object to standard surreal
|| form.
  x $naive_plus y = (x_int $int_plus y_int,
                     x_frac $rev_frac_plus y_frac)
                     where (x_int,x_frac) = intrevfrac x
                           (y_int,y_frac) = intrevfrac y

int_plus :: rep_surreal -> rep_surreal -> rep_surreal
|| adds two pure integer sign-expansions, each consisting
|| solely of the one sign (though one might be all pluses
|| and the other all minuses).
  [] $int_plus y = y
  x $int_plus [] = x
  (s:rest_x) $int_plus (s:rest_y)
    = s:s:(rest_x $int_plus rest_y)
  (s:rest_x) $int_plus (t:rest_y)
    = rest_x $int_plus rest_y

rev_frac_plus :: rep_surreal -> rep_surreal -> twisted_surreal
|| adds two fractional parts, where the signs descend from
|| 1/2 in powers of two, to a twisted fractional part where
|| the signs may include zeroes and descend from 1 in powers
|| of two.

  || if one stream finishes, the other can just be echoed
  [] $rev_frac_plus y = '0':y
  x $rev_frac_plus [] = '0':x

  || both signs the same: echo that sign
  (s:rest_x) $rev_frac_plus (s:rest_y)
    = s:(rest_x $rev_frac_plus rest_y)

  || both signs different: output a zero since they cancel
  (s:rest_x) $rev_frac_plus (t:rest_y)
    = '0':(rest_x $rev_frac_plus rest_y)

tidyup :: (rep_surreal, twisted_surreal) -> rep_surreal
|| tidies up the temporary answer from naive_plus with its
|| separate integer and fractional parts, and its possible
|| zeroes among the signs of the fractional part.
  tidyup (s:s:s:intpart, revfracpart)
    = s:tidyup (s:s:intpart, revfracpart)
  tidyup (intpart, revfracpart)
    = blend intpart (normalize revfracpart)

normalize :: twisted_surreal -> rep_surreal
|| given an input stream, possibly with zeroes as well as 
|| pluses and minuses, computes a stream of equal value made
|| only of pluses and minuses.
  normalize = purge_zeroes 0

purge_zeroes :: num -> twisted_surreal -> rep_surreal
|| auxiliary function called by "normalize". The numeric
|| parameter is the number of zeroes "queued" waiting for a
|| sign to appear, whereupon they can be dumped correctly.

  || if a zero appears, queue it
  purge_zeroes n ('0':rest) = purge_zeroes (n+1) rest

  || if a sign appears with no zeroes queued, echo it
  purge_zeroes 0 (s:rest) = s:(purge_zeroes 0 rest)

  || output n zeroes then sign s as s then n of the
  || opposite sign to s---this preserves the value
  purge_zeroes n (s:rest)
    = s:(rep n (opposite s))               
      ++ purge_zeroes 0 rest

  || on end-of-stream, ignore queued zeroes and finish
  purge_zeroes n [] = []

blend :: rep_surreal -> rep_surreal -> rep_surreal
|| blends an integer and fractional part into a surreal
|| answer. The fractional part has been "purified" by
|| function normalize above, and consists only of pluses and
|| minuses, of value 1, 1/2, 1/4,..... Care must be taken 
|| that only values which definitely can't be overturned by
|| the future part of the stream are output at any given 
|| stage.

  || stream of length 1 or less
  blend intpart []       = intpart
  blend intpart [s]      = intpart $int_plus [s]

  || stream of length 2 or more
  || note: answer streams are finished surreals rather than
  || isolated fractional parts, and must be read in the 
  || "unary/binary" way
  blend [] (s:s:rest)    = s:s:(opposite s):rest
  blend [] (s:t:rest)    = s:t:rest
  blend [s] (s:s:rest)   = s:s:s:(opposite s):rest
  blend [s] (s:t:rest)   = s:s:t:rest
  blend [s] (t:u:rest)   = u:(opposite u):rest
  blend [s,s] (s:s:rest) = s:s:s:s:(opposite s):rest
  blend [s,s] (s:t:rest) = s:s:s:t:rest
  blend [s,s] (t:s:rest) = s:s:t:rest
  blend [s,s] (t:t:rest) = s:t:rest

|| supporting operations for multiplication

intfractimes :: (rep_surreal, rep_surreal) -> (rep_surreal, rep_surreal)
                                 -> num -> num -> rep_surreal
|| The value of intfractimes (xi, xf) (yi, yf) a b
|| is (a+x) * (b+y) - a * b, where x=xi+xf is the sum of
|| the integer and fractional parts given in the first
|| argument and y=yi+yf is likewise for the second
|| argument. 

|| The motivation here is to optimize the execution pattern
|| for lazy evaluation: a and b give the amounts of integer
|| part already "eaten" off the two input streams, at which
|| point a*b pluses can permissibly be output. Assuming they
|| have indeed been output, the remaining term must be equal
|| to the original product MINUS a*b, hence the above
|| expression.

|| Note: the expression is analogous to an invariant for an
|| imperative program.

  || '+' available on both streams:
  || output (a+1)*(b+1)-a*b = (a+b+1) extra pluses
  intfractimes ('+':intx, fracx) ('+':inty, fracy) a b
    = rep (a+b+1) '+'              
      ++ intfractimes (intx, fracx) (inty, fracy) (a+1) (b+1)

  || '+' available on second stream only:
  || output a*(b+1)-a*b = a extra pluses
  intfractimes ([], fracx) ('+':inty, fracy) a b
    = rep a '+'            
      ++ intfractimes ([], fracx) (inty, fracy) a (b+1)

  || '+' available on first stream only:
  || output (a+1)*b-a*b = b extra pluses
  intfractimes ('+':intx, fracx) ([], fracy) a b
    = rep b '+'             
      ++ intfractimes (intx, fracx) ([], fracy) (a+1) b

  || both streams' integer parts exhausted
  || no fractional part: answer is a*b-a*b = 0
  intfractimes ([], []) ([], []) a b = []

  || general case: convert to binary then back again at end
  intfractimes ([], fracx) ([], fracy) a b
    = remove_intpart (a*b)
                     ((a, fracx) $binary_times (b, fracy))

remove_intpart :: num -> (bitstream, num) -> rep_surreal
|| receives the quantity of pluses already printed by
|| intfractimes (a*b) and a coded answer to the whole
|| problem in bitstream form. Converts to standard surreal
|| form BUT misses out the specified number of pluses (since
|| intfractimes has already printed them).
  remove_intpart n x
    = rep (intpart-n) '+'             
      ++ normalize ('0':fracpart)
      where (intpart, fracpart) = binary_intfrac x

binary_times :: (num, rep_surreal) -> (num, rep_surreal)
                                -> (bitstream, num)
|| takes two surreals, with their integer and fractional
|| parts already separated out, and computes the product in
|| binary form. The number in the output is a floating point
|| offset saying how many binary places the bitstream must
|| be shifted UP (never down).
  a $binary_times b
    = (frac_answer, offset_a + offset_b)
      where
      (stream_a, offset_a) = make_binary_frac a
      (stream_b, offset_b) = make_binary_frac b
      frac_answer = stream_a $binary_frac_times stream_b

binary_frac_times :: bitstream -> bitstream -> bitstream
|| takes two bitstreams representing binary fractional parts
|| and computes their product, also as a binary fraction.
|| The streams may be finite or infinite independently.
  x $binary_frac_times y = binary_frac_accumulate x y "0" []

binary_frac_accumulate :: bitstream -> bitstream -> bitstream
                            -> [bitstream] -> bitstream
|| first arg -> second arg -> state buffer
||                   -> future contributions list -> answer!

|| To multiply possibly infinite streams without rounding 
|| off at any stage, great care is needed and a great deal
|| of state information must be carried around. The "state
|| buffer" holds the digits which are destined to be
|| output. However, the only ones which CAN be output on
|| each cycle are those which a run-time analysis shows
|| CAN'T be altered in value by the entire sum, present and
|| future, of the "future contributions list". The price of
|| outputting an alterable digit could be an irreversibly
|| wrong answer stuck on the screen for the user to see.

|| This laborious computation at each cycle is what makes
|| "times" so slow. It's unavoidable if infinite streams are
|| to be handled by lazy evaluation. (FINITE streams can be
|| handled by various standard algorithms in the literature
|| which would be far faster.)

  || all streams finished: just dump the state buffer
  binary_frac_accumulate x [] s [] = s

  || second argument but not future contributions list
  || exhausted: strip heads from future contributions list
  binary_frac_accumulate x [] s l
    = allowed_output ++ (binary_frac_accumulate x [] s' l')
      where
      (sum_of_heads, boosted_length, l') = strip_heads l
      (allowed_output, s') = update_state_buffer
                             (s++"0") 
                             sum_of_heads
                             boosted_length

  || next digit zero: add nothing to future contributions
  || list, but strip heads to compute next allowed output
  binary_frac_accumulate x ('0':y) s l 
    = allowed_output ++ (binary_frac_accumulate x y s' l')
      where
      (sum_of_heads, boosted_length, l') = strip_heads l
      (allowed_output, s') = update_state_buffer
                             (s++"0")
                             sum_of_heads
                             boosted_length

  || next digit one: add a copy of first argument to future
  || contributions list, then strip heads and compute next
  || allowed output
  binary_frac_accumulate x ('+':y) s l 
    = allowed_output ++ (binary_frac_accumulate x y s' l')
      where
      (sum_of_heads, boosted_length, l') = strip_heads (x:l)
      (allowed_output, s') = update_state_buffer
                             (s++"0")
                             sum_of_heads
                             boosted_length

binary_intfrac :: (bitstream, num) -> (num, bitstream)
|| separates a bitstream with floating-point offset into its
|| integer and fractional parts
  binary_intfrac = binary_accumulate 0

binary_accumulate :: num -> (bitstream, num)
                          -> (num, bitstream)
|| separates out the integer and fractional parts on behalf
|| of binary_intfrac using an accumulating parameter for the
|| integer part
  binary_accumulate intpart (stream, 0) = (intpart, stream)
  binary_accumulate intpart ('0':stream, count)
    = binary_accumulate (2*intpart)   (stream, count-1)
  binary_accumulate intpart ('+':stream, count)
    = binary_accumulate (2*intpart+1) (stream, count-1)

strip_heads :: [bitstream] -> (num, num, [bitstream])
|| This is a key function in the analysis of what digits in
|| the state buffer can and can't be output. It takes in the
|| future contributions list, holding all future digits yet
|| computed for later absorption into the answer, and strips
|| the heads of the component lists, these heads being the
|| digits of the current binary column reached. It returns
|| the sum of these heads and the stripped list.

|| HOWEVER, you can't just naively add these to the state
|| and produce the new state. You have to know what the
|| maximum EXTRA value that COULD ever hit the state is.
|| (This can then be added as a worst case and any digits
|| that survive this can, and indeed must, be output.)

|| So this theoretical maximum value is also computed here.
|| It can be proved to be simply the length of the stripped
|| list plus 2. This is quite easy to compute during the
|| walk down the list.

  || "0" destroyed by stripping heads and contributes
  || nothing to sum, so drop it
  strip_heads ("0":l) = strip_heads l

  || "+" destroyed by stripping heads but contributes 1 to
  || sum, so record this
  strip_heads ("+":l)
    = (sum_of_heads+1, boosted_length, l')
      where 
      (sum_of_heads, boosted_length, l') = strip_heads l

  || "0..." survives head-stripping and adds 1 to length,
  || but begins with zero and doesn't add to sum
  strip_heads (('0':x:rest):l)
    = (sum_of_heads, boosted_length+1, (x:rest):l')
      where
      (sum_of_heads, boosted_length, l') = strip_heads l

  || "+..." survives head-stripping and adds 1 to length,
  || and also adds 1 to sum
  strip_heads (('+':x:rest):l)
    = (sum_of_heads+1, boosted_length+1, (x:rest):l')
      where
      (sum_of_heads, boosted_length, l') = strip_heads l

  || base case: empty future contributions list
  strip_heads [] = (0, 2, [])

binary_reverse_add :: bitstream -> bitstream
                                 -> twisted_bitstream
|| reversed state -> reversed extra -> forwards new state,
|| possibly starting with overflow indicator ('2')

|| This function adds the "extra" (coming in from the future
|| contributions list) to the existing state, producing the
|| new state with possible overflow. This allows the system
|| to progress from state to state, and also to see how
|| much of the state is left undamaged even in the worst
|| case.

|| (For internal purposes the state and extra are reversed.)
  binary_reverse_add state extra
    = b_r_a_accumulate state extra [] 0

b_r_a_accumulate :: bitstream -> bitstream
                     -> twisted_bitstream -> num
                      -> twisted_bitstream
|| reversed state -> reversed extra -> accumulating answer
||  -> current carry -> forwards new state, possibly with
||   overflow

|| This one looks formidable I admit, but essentially it's
|| just a simple little finite-state machine, plodding
|| through the various possible combinations of first
|| digit, second digit and carry to produce the answer digit
|| and new carry on each cycle.

  || cases when state length >= 2
  || state length >= 2, starting with '0'
  b_r_a_accumulate ('0':x:state) ('0':extra) answer 0
    = b_r_a_accumulate (x:state) extra ('0':answer) 0
  b_r_a_accumulate ('0':x:state) ('0':extra) answer 1
    = b_r_a_accumulate (x:state) extra ('+':answer) 0
  b_r_a_accumulate ('0':x:state) ('+':extra) answer 0
    = b_r_a_accumulate (x:state) extra ('+':answer) 0
  b_r_a_accumulate ('0':x:state) ('+':extra) answer 1
    = b_r_a_accumulate (x:state) extra ('0':answer) 1
  b_r_a_accumulate ('0':x:state) [] answer 0
    = b_r_a_accumulate (x:state) [] ('0':answer) 0
  b_r_a_accumulate ('0':x:state) [] answer 1
    = b_r_a_accumulate (x:state) [] ('+':answer) 0

  || state length >= 2, starting with '+'
  b_r_a_accumulate ('+':x:state) ('0':extra) answer 0
    = b_r_a_accumulate (x:state) extra ('+':answer) 0
  b_r_a_accumulate ('+':x:state) ('0':extra) answer 1
    = b_r_a_accumulate (x:state) extra ('0':answer) 1
  b_r_a_accumulate ('+':x:state) ('+':extra) answer 0
    = b_r_a_accumulate (x:state) extra ('0':answer) 1
  b_r_a_accumulate ('+':x:state) ('+':extra) answer 1
    = b_r_a_accumulate (x:state) extra ('+':answer) 1
  b_r_a_accumulate ('+':x:state) [] answer 0
    = b_r_a_accumulate (x:state) [] ('+':answer) 0
  b_r_a_accumulate ('+':x:state) [] answer 1
    = b_r_a_accumulate (x:state) [] ('0':answer) 1

  || state length 1
  || state="0"; excludes length(extra)>=2
  b_r_a_accumulate "0" []  answer 0 = '0':answer
  b_r_a_accumulate "0" []  answer 1 = '+':answer
  b_r_a_accumulate "0" "0" answer 0 = '0':answer
  b_r_a_accumulate "0" "0" answer 1 = '+':answer
  b_r_a_accumulate "0" "+" answer 0 = '+':answer
  b_r_a_accumulate "0" "+" answer 1 = '2':answer

  || state="+"; excludes length(extra)>=2
  b_r_a_accumulate "+" []  answer 0     = '+':answer
  b_r_a_accumulate "+" []  answer 1     = '2':answer
  b_r_a_accumulate "+" "0" answer 0     = '+':answer
  b_r_a_accumulate "+" "0" answer 1     = '2':answer
  b_r_a_accumulate "+" "+" answer carry = '2':answer

  || state="0"|"+"; length(extra)>=2
  b_r_a_accumulate [state] (x:y:extra) answer carry
    = '2':answer

  || for completeness an empty state is handled, though this
  || never arises in the particular applications invoked in
  || this package
  || state length 0
  b_r_a_accumulate [] extra answer carry = answer

update_state_buffer :: bitstream -> num -> num
                                  -> (bitstream, bitstream)
|| state -> sum_of_heads -> boosted_length
||                        -> (allowed output, new state)

|| Here the state is actually updated and the allowed output
|| and next state are computed. The INTERNAL new state is
|| simply the old state plus the sum of heads. To see how
|| much can be made EXTERNAL---ie, output---even in the
|| worst case, we add the worst-case parameter, called
|| "boosted_length" here, and find what stays the same and
|| what gets damaged. The undamaged bit is the allowed 
|| output, and the damaged bit is the new state which must
|| be held for the next major cycle.

  update_state_buffer state sum_of_heads boosted_length
    = (pluses++same, different)
      where
      || new INTERNAL state, by simple addition
      state' = binary_reverse_add
               (reverse state)
               (reverse (binary_integer sum_of_heads))
      || pluses at the beginning of the state can and must
      || always be immediately output; eg, if the state is
      || "+++0+00+", the three pluses can't go any higher,
      || since '+' is the highest binary digit, so they've
      || taken on their final values and are ready for
      || output.
      (pluses, rest) = strip_pluses state'
      || create temporary state "state''" by adding in the
      || worst-case extra amount, ready for comparison in
      || order to find what parts are damaged and
      || undamaged.
      state'' = binary_reverse_add
                (reverse rest)
                (reverse (binary_integer
                               boosted_length))
      || parts that stay the same are ready for output;
      || parts that change are the new state.
      (same, different) = find_differences rest state''

find_differences :: bitstream -> twisted_bitstream
                               -> (bitstream, bitstream)
|| takes in the current and worst-case state and computes
|| the parts of the current state that are the same and
|| different, respectively, when compared with the worst-
|| -case state.
  find_differences (x:rest1) (x:rest2)
    = (x:same, different)
      where (same, different) = find_differences rest1 rest2
  find_differences (x:rest1) (y:rest2) = ([], x:rest1)
  find_differences [] [] = ([], [])

make_binary_frac :: (num, rep_surreal) -> (bitstream, num)
|| works out the stream-based (ie, possibly infinite)
|| floating-point binary representation for a given surreal
|| which has already been separated out into its integer and
|| fractional parts.
  make_binary_frac (intpart, fracpart)
    = (binary_intpart ++ binary_fracpart,
       # binary_intpart)
      where
      binary_intpart  = binary_integer intpart
      binary_fracpart = binary_normalize fracpart

binary_normalize :: rep_surreal -> bitstream
|| like "normalize", but this time it takes a fractional
|| surreal in standard sign-expansion form and turns it
|| into a bitstream.
  binary_normalize [] = []
  binary_normalize ('+':'-':rest) = binary_sequence rest

binary_sequence :: rep_surreal -> bitstream
|| auxiliary function used by binary_normalize
|| uses the description given in Conway [1976] to convert
|| a stream of signs beyond the initial "+-" into the
|| equivalent stream of bits
  binary_sequence ('+':rest) = '+':binary_sequence rest
  binary_sequence ('-':rest) = '0':binary_sequence rest
  binary_sequence [] = "+"

|| supporting operations for reciprocal

get_reciprocal :: num -> num -> rep_surreal -> surreal
|| accumulates estimates of the numerator and denominator of
|| the given surreal in the first two parameters, until the
|| surreal is exhausted and they are known exactly.
|| The reciprocal is then computed using conversion function
|| "over". This is why "reciprocal" only handles dyadic
|| fractions---the surreal here MUST terminate!
  || surreal not yet exhausted: improve current estimates
  get_reciprocal x 1 ('+':rest) 
    = get_reciprocal (x+1) 1 rest
  get_reciprocal x 1 ('-':rest)
    = get_reciprocal (2*x-1) 2 rest
  get_reciprocal x y ('+':rest)
    = get_reciprocal (2*x+1) (2*y) rest
  get_reciprocal x y ('-':rest)
    = get_reciprocal (2*x-1) (2*y) rest

  || surreal exhausted: swap numerator and denominator and
  || exit
  get_reciprocal x y [] = y $over x

|| support functions for the conversion facilities

naive_over :: num -> num -> rep_surreal
|| for a ratio destined to be in the range [0..1), computes
|| the binary stream by repeated doubling and subtraction
  x $naive_over y
    = [], x=0
    = '0':((x+x) $naive_over y), x<y
    = '+':((z+z) $naive_over y), x>=y
      where z=x-y

approximation_stream :: num -> num -> rep_surreal -> [num]
|| Using the first two parameters as accumulating parameters,
|| this function takes a surreal and produces the (possibly
|| infinite) stream of successive approximations got by
|| truncating the sign-expansion at each point. These
|| approximations tend towards the true value.

|| The first parameter is the latest approximation and the
|| second is the latest adjustment made over the previous
|| approximation.

  || '+' in integer part: continue adding 1
  approximation_stream sofar 1 ('+':rest)
    = sofar:(approximation_stream (sofar+1) 1 rest)

  || '-' after integer part: switch to subtracting 1/2
  approximation_stream sofar 1 ('-':rest)
    = sofar:(approximation_stream (sofar-0.5) 0.5 rest)

  || '+' in fractional part: latest adjustment is half the
  || previous adjustment, and in the upwards direction
  approximation_stream sofar frac ('+':rest)
    = sofar:(approximation_stream
              (sofar+newfrac) newfrac rest)
      where newfrac = frac / 2

  || '-' in fractional part: latest adjustment is half the
  || previous adjustment, and in the downwards direction
  approximation_stream sofar frac ('-':rest)
    = sofar:(approximation_stream
              (sofar-newfrac) newfrac rest)
      where newfrac = frac / 2

  || if surreal finishes, exact value can be output directly
  approximation_stream sofar latest_change [] = [sofar]



|| auxiliary functions on sign-expansions, bitstreams etc

|| these play a general supporting role, being basic to many
|| of the major functions' initialization or cycling
|| behaviour.

intfrac :: rep_surreal -> (rep_surreal, rep_surreal)
|| splits a surreal into an integer and fractional part,
|| with the fractional part of the SAME sign as the integer
|| part.
  intfrac [] = ([], [])
  intfrac [s] = ([s], [])
  intfrac (s:s:rest)
    = (s:intpart, fracpart)
      where
      (intpart, fracpart) = intfrac (s:rest)
  intfrac (s:t:rest) = ([], s:t:rest)

intrevfrac :: rep_surreal -> (rep_surreal, rep_surreal)
|| splits a surreal into an integer and fractional part,
|| with the fractional part of the OPPOSITE sign to the
|| integer part. Note: "rev" in the name is not intended to
|| hint the list itself is reversed, only the sign!
  intrevfrac [] = ([], [])
  intrevfrac [s] = ([s], [])
  intrevfrac (s:s:rest)
    = (s:intpart, revfracpart)
      where
      (intpart, revfracpart) = intrevfrac (s:rest)
  intrevfrac (s:t:rest) = ([s], t:rest)

strip_pluses :: bitstream -> (bitstream, bitstream)
|| splits a bitstream into the longest initial contiguous
|| block of pluses, followed by the rest. eg, strip_pluses
|| "+++++0+00+0" = ("+++++", "0+00+0"). This is used during
|| multiplication to decide how much of the state buffer can
|| safely be output.
  strip_pluses ('+':b)
    = ('+':pluses, rest)
      where (pluses, rest) = strip_pluses b
  strip_pluses ('0':b) = ([], '0':b)
  strip_pluses [] = ([], [])

binary_integer :: num -> bitstream
|| expresses a non-negative integer in binary form
  binary_integer n = binary_integer_accumulate n []

binary_integer_accumulate :: num -> bitstream -> bitstream
|| converts an integer to binary on behalf of 
|| "binary_integer" using an accumulating parameter
  binary_integer_accumulate n answer
    = binary_integer_accumulate
      (n div 2)
      ((bit_rep (n mod 2)):answer), n>0
    = answer, n=0







|| LOW-LEVEL OPERATIONS

opposite :: sign -> sign
|| returns the opposite of a given sign
  opposite '+' = '-'
  opposite '-' = '+'

bit_rep :: num -> symbolic_bit
|| returns the bitstream character representation of a bit
  bit_rep 0 = '0'
  bit_rep 1 = '+'

limiting_value :: [*] -> *
|| returns the limit of a list (detected as when the members
|| become identical up to the system's resolution, or as
|| just the last member if the list is finite)
|| slightly more comprehensive than the built-in "limit"
  limiting_value (a:b:rest)
    = a, a=b
    = limiting_value (b:rest), otherwise
  limiting_value [a] = a
  limiting_value []
    = error "No values for limiting_value to work on"


|| print-representation for type surreal 

|| showsurreal :: surreal -> [char]
|| Miranda interface to built-in function "show"
  showsurreal = ("SURREAL "++)
@