(t mod 2)::(add' l l' (t div 2)) ; fun zeros k = if k<=0 then [] else 0::zeros(k-1) ; fun add r r' = let val (l,l') = (prune r, prune r') val k = length l' - length l in prune (add' ((zeros k)@l) ((zeros(~k))@l') 0) end ; fun safeAdd r r' = SOME (add r r') handle One => NONE ; (* Dividing dyadic rationals by 2^k *) fun scaleDown l k = l@(zeros k) ; fun twoToMinus k = if k>0 then 1::(zeros(k-1)) else raise One ; (* We can now do integration by creeping along the unit interval from left to right: *) fun integrate' (F:Real->Real) n (r:Dyadic) (acc:Dyadic) = case ModMax (fn a => approx n (F a)) (mkReal r) of (y,NONE) => y | (y,SOME k) => let val acc' = add acc (scaleDown y (k+1)) and r' = safeAdd r (twoToMinus(k+1)) in case r' of NONE => acc' | SOME r'' => integrate' F n r'' acc' (* this is tail-recursive *) end ; fun integrate F n = (integrate' F n Dzero Dzero, twoToMinus n) ; (* This computes the integral of F to within 2^-n. Returns the "best known answer" as a dyadic rational together with its error margin. The following function lets us see this information in a reasonable way: *) fun machineSpread (x,e) = let val (x',_) = machineReal x and (e',_) = machineReal e in (x'-e', x'+e') end ; (* A bit more work would be needed to compute the integral of F as an exact real number (i.e. a sequence of digits -1,0,1). One interesting question is whether the above algorithm can be modified to compute the integral *incrementally* in a reasonable way. But it seems unlikely we can do this without massive use of memory space. Unfortunately, since we haven't implemented any other real-number operations, we can't yet write any interesting functions to try this on! Meanwhile, here are some boring functions. *) fun id x = x ; fun c x = Rthird ; integrate id 10 ; machineSpread it ; integrate c 10 ; machineSpread it ; (* Quite surprisingly, the above integration operation can be performed in Pure ML, using the very clever Berger-Gandy modulus functional. See for example Alex Simpson's paper "Lazy Functional Algorithms for Exact Real Functionals", available e.g. from ftp://ftp.dcs.ed.ac.uk/pub/als/Research/ However, there are several advantages to doing it our way: - it's easier to understand (I hope!) - it ought to be considerably more efficient, at least in certain cases (though we haven't tested this out yet) - with some slight modifications, our method can be used to integrate functions which (I believe) can't be integrated in Pure ML: e.g. (partial) functions with a single discontinuity; functions on the open interval (0,1) with bounded range; certain functions with Kleene singularities, that aren't total on the classical reals. *) (* Another operation that we can perform using Mod but definitely can't perform in Pure ML is the following: Write a function ([0,1] -> unit) -> [0,1] which, given a function f such that f(a) diverges but f(b) terminates for every b<>a, returns a. I don't know whether this is useful, but it's quite interesting. *) (* 5. ADVANCED STUFF. *) (* We next give a more complicated example of a sequentially realizable function E, which I believe isn't definable from Mod (equivalently from F). *) (* First think about the type of streams over int. These can be identified with functions f:int -> int such that if f(n) is undefined then so is f(m) for all m>n. (We ignore values of f(n) for n<0.) *) datatype Stream = str of unit -> (int * Stream) ; fun streamToFun (str s) 0 = fst(s()) | streamToFun (str s) n = streamToFun (snd(s())) (n-1) ; fun funToStream f = str (fn () => (f 0, funToStream (fn n => f(n-1)))) ; (* Now think about sequential functions G : Stream -> int. Any such function is computed by an intensional strategy which can only ask for values of the stream in the correct order. We may think of such a strategy as a countably-branching tree (possibly with infinite paths) whose leaves are labelled with "answers" (or with "bottom"), and whose other nodes are labelled with "questions". In fact, a question at depth d will always be the one that asks for the d'th element of the stream. A very nice property of the type Stream -> int is that for any extensional function G there is a *canonical* (i.e. smallest) such intensional strategy that computes it - namely the one in which any subtree containing no answers is replaced by bottom. This means that if we can write a program that returns a finite amount of "positive information" about the strategy, this will automatically be functional. *) (* Some stuff associated with these strategies: *) type Node = int list ; datatype Label = Q of int | A of int ; type LabNode = Node * Label ; (* A "sort" function for lists of pairs (a,b) according to a given total order leq on their first components. Silently removes duplicates (a,b),(a,b). Doesn't check for inconsistencies (a,b),(a,b') where b<>b'. (N.B. We will only use this function when we know there aren't any such inconsistencies, though some thought is required to see this!) *) fun insert leq x [] = [x] | insert leq x (l as h::t) = if fst x = fst h then l else if leq (fst x) (fst h) then x::l else h::(insert leq x t) ; fun lookup x [] = NONE | lookup x ((x',y)::l) = if x=x' then SOME y else lookup x l ; fun sort leq [] = [] | sort leq (h::t) = insert leq h (sort leq t) ; (* Two orderings that will be used in conjunction with the above function. A simple lexicographic ordering on lists... *) fun lessOrEq (x:int) x' = (x<=x) ; fun lexLeq [] _ = true | lexLeq _ [] = false | lexLeq (h::t) (h'::t') = (lessOrEq h h') andalso (lexLeq t t') ; (* ...and a similar ordering on lists of pairs. *) fun lex1Leq [] _ = true | lex1Leq _ [] = false | lex1Leq ((x,y)::t) ((x',y')::t') = (lessOrEq x x') andalso (lex1Leq t t') ; (* Given an ordered list of labelled nodes (sorted lexicographically), we wish to see if they constitute a well-formed tree. "Well-formed" here means it's prefix-closed, all leaves are labelled by answers (A a), and all other nodes are labelled by questions (Q x). It will also follow from the way our trees are constructed that the same question will never be asked twice along the same path. The following operation splits up such a list into lists corresponding to the immediate subtrees. *) local fun takeSubtree h [] = ([],[]) | takeSubtree h (([],_)::_) = raise Bug (* shouldn't arise *) | takeSubtree h (l as (((h'::t),lab)::l')) = if h<>h' then ([],l) else case takeSubtree h l' of (s,l'') => ((t,lab)::s,l'') in fun subtrees [] = [] | subtrees (([],_)::l) = raise Bug | subtrees (l as (((h::t),lab)::l')) = case takeSubtree h l of (s,l'') => (h,s)::(subtrees l'') end ; (* We can now convert a list of labelled nodes into the type 2 graph arising from the corresponding tree. This graph consists of all pairs (g1,a) where a is the answer on some leaf and g is the type 1 graph corresponding to the path leading to this leaf. Conceptually we have list of labelled nodes --> tree --> type 2 graph. In our implementation we don't explicitly construct the intermediate tree, though we do check in passing that the tree is well-formed (we raise an exception if it's not). *) exception BadTree ; fun applyToAll l f = fold op@ (map f l) [] ; local fun makeGraph2' g1 [] = raise BadTree | makeGraph2' g1 (([],A a)::_) = [(g1,a)] | makeGraph2' g1 (([],Q x)::t) = applyToAll (subtrees t) (fn (h,s) => makeGraph2' (insert lessOrEq (x,h) g1) s) | makeGraph2' g1 ((_::_,_)::_) = raise BadTree in fun makeGraph2 [] = [] | makeGraph2 l = makeGraph2' [] l end ; (* Actually, in the graph g2 that this returns, each g1 will be sorted though g2 itself won't be. But we do this below. *) (* Now the interesting bit: the functional E. This takes as arguments a type 2 function G, and an "exploration": a kind of strategy for exploring the intensional strategy used by G. Returns some *extensional* information about G on the basis of what it discovers. This will take the form of a graph for some finite approximation to G. The graph will be suitably sanitized (i.e. hereditarily sorted) so that we can't learn anything about the evaluation order used by G. The version of E here also returns a "result" of type 'a, dictated by the strategy. This doesn't increase the expressive power of E, but might be useful in practice. *) datatype 'a Exploration = Answer of 'a | Question of Node * (Label -> 'a Exploration) ; fun E expl G = let exception Alarm of int fun fnWithScript script = fn x => let val (oldpairs,newvals) = !script in case lookup x oldpairs of (SOME y) => y | NONE => case newvals of (h::t) => (script:=((x,h)::oldpairs,t) ; h) | [] => raise Alarm x end fun E_aux (Answer a) labnodes = (a, labnodes) | E_aux (Question (node, seed)) labnodes = let val label = A (G (funToStream (fnWithScript (ref ([],node))))) handle Alarm x => Q x in E_aux (seed label) ((node,label)::labnodes) end in case E_aux expl [] of (a, labnodes) => (a, sort lex1Leq (makeGraph2 (sort lexLeq labnodes))) handle BadTree => bot() end ; (* So far I haven't implemented any applications of this functional. I believe there are some things one can do with E that one can't do with Mod - e.g. integrating real-valued functions with a limited number of discontinuities - but they're a bit complicated. If anyone can think of other natural applications of E I'd be very interested. *) (* Even E isn't strong enough to define all sequentially realizable functionals. However, there does exist a "universal" sequentially realizable functional H, of type level 3, such that any other s.r. functional is definable from H in Pure ML. (For a definition of H and proof of this property, see the theory paper mentioned above.) H is a bit like E, only worse because instead of Stream->int we have the whole of (int->int)->int, so the evaluation order isn't predictable. From a practical point of view, the main disadvantage of H is one of complexity: intuitively it involves a factorial size search in the worst case. I implemented H in ML a while ago, but while writing the theory paper I discovered some subtleties I'd overlooked, which mean the implementation is wrong. I haven't got round to reworking it yet. The existence of H is theoretically very interesting, but at present I don't know of any natural applications for which E does not suffice. *) (* End of file *)