OKlibrary  0.2.1.6
SurrealNumbers.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 31.5.2011 (Swansea) */
00002 /* Copyright 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00023 
00024 /* ******************************************
00025    * The basic notion of a "surreal number" *
00026    ******************************************
00027 */
00028 
00029 /* The intuitive notion of a "surreal number" x ("surnum") is
00030    that it is a pair x = (x_1,x_2), where x_1, x_2 are sets
00031    of surreal numbers, such that for all a in x_1 and for all b in x_2
00032    we have a < b.
00033 
00034    So in parallel we need to define "x < y" for surreal numbers.
00035    It seems more convenient to define "x <= y", and then to define
00036    x < y <=> x <= y und not (y <= x).
00037 
00038   Now x <= y is defined to hold if
00039    - for all a in x_1 we have a < y
00040    - for all b in y_2 we have x < b.
00041 
00042   This expresses exactly all the relations we know that hold for sure,
00043   since x_1 is a set of lower bounds for x, while y_2 is a set of
00044   upper bounds for y; note that x_2 as well as y_1 does not yield any
00045   information here.
00046 
00047   The induced equivalence relation x ~ y is defined as usual as
00048   x <= y and y <= x.
00049 
00050   For a given universe U (of set theory) we have the set SQ_U of all
00051   such surreal numbers in U, where "SQ" stands for "surreal quasi", since
00052   <= for surreal numbers is only a quasiorder, and the true surreal numbers
00053   are the equivalence classes within U w.r.t. ~.
00054 */
00055 
00056 /* Whether x is a "surreal number": */
00057 surnum_p(x) := listp(x) and is(length(x)=2) and
00058  every_s(surnum_p,first(x)) and every_s(surnum_p,second(x)) and
00059  block([res : true],
00060    for a in first(x) while res do
00061      for b in second(x) while res do
00062        if not surnum_ltp(a,b) then res : false,
00063    res)$
00064 
00065 /* Whether for surreal numbers x, y we have x <= y : */
00066 surnum_lep(x,y) :=
00067  every_s(lambda([a], surnum_ltp(a,y)), first(x)) and
00068  every_s(lambda([b], surnum_ltp(x,b)), second(y))$
00069 
00070 /* Whether for surreal numbers x, y we have x < y : */
00071 surnum_ltp(x,y) := not surnum_lep(y,x)$
00072 
00073 /* All surreal numbers (in all presentations) created at "epoche <= n": */
00074 epoche_surnum(n) := block(
00075  [prev : powerset(if n=0 then {} else epoche_surnum(n-1))],
00076   subset(cartesian_product(prev,prev), surnum_p))$
00077 
00078 /* The induced equivalence-relation x ~ y (when two surreal numbers are to be
00079    considered "equal"):
00080 */
00081 surnum_equalp(x,y) := surnum_lep(x,y) and surnum_lep(y,x)$
00082 
00083 /* The equivalence classes of surreal numbers created up to epoche n: */
00084 eqc_epoche_surnum(n) := equiv_classes(epoche_surnum(n), surnum_equalp)$
00085 
00086 
00087 /* ***************************
00088    * Arithmetical operations *
00089    ***************************
00090 */
00091 
00092 /* x + y : */
00093 surnum_add(x,y) := [
00094  union(map(lambda([a], surnum_add(a,y)), first(x)), 
00095        map(lambda([a], surnum_add(x,a)), first(y))),
00096   union(map(lambda([a], surnum_add(a,y)), second(x)), 
00097         map(lambda([a], surnum_add(x,a)), second(y)))
00098 ]$
00099 
00100 /* -x : */
00101 surnum_neg1(x) := [map(surnum_neg1, second(x)), map(surnum_neg1, first(x))]$
00102 /* x - y : */
00103 surnum_neg2(x,y) := surnum_add(x,surnum_neg1(y))$
00104 
00105 /* x * y : */
00106 surnum_prod(x,y) := [
00107  union(map(lambda([p], surnum_neg2(surnum_add(surnum_prod(p[1],y),surnum_prod(x,p[2])), surnum_prod(p[1],p[2]))), cartesian_product(first(x),first(y))),
00108        map(lambda([p], surnum_neg2(surnum_add(surnum_prod(p[1],y),surnum_prod(x,p[2])), surnum_prod(p[1],p[2]))), cartesian_product(second(x),second(y)))),
00109  union(map(lambda([p], surnum_neg2(surnum_add(surnum_prod(p[1],y),surnum_prod(x,p[2])), surnum_prod(p[1],p[2]))), cartesian_product(first(x),second(y))),
00110        map(lambda([p], surnum_neg2(surnum_add(surnum_prod(p[1],y),surnum_prod(x,p[2])), surnum_prod(p[1],p[2]))), cartesian_product(second(x),first(y))))
00111 ]$
00112 
00113 
00114 /* ***************
00115    * Conversions *
00116    ***************
00117 */
00118 
00119 /* n >= 0 as surreal number: */
00120 nat2surnum(n) := [setify(create_list(nat2surnum(i),i,0,n-1)), {}]$
00121 /* For n >= 0 the negative integer -n as surreal number: */
00122 nnat2surnum(n) := [{}, setify(create_list(nnat2surnum(i),i,0,n-1))]$
00123 /* Note nnat2surnum(n) = surnum_neg1(nat2surnum(n)). */
00124 /* Integers as surreal numbers: */
00125 int2surnum(z) := if z >= 0 then nat2surnum(z) else nnat2surnum(-z)$
00126