Below are the 20 most recent journal entries recorded in r6research's LiveJournal:

[ << Previous 20 ]

Thursday, May 28th, 2009
5:05 pm	Classical Propositions Have at Most One Proof I claimed that all classical propositions have at most one proof upto extensionality. My supervisor wanted to know if I could prove, or even state it in Coq. Below is my proof. I add an extensionality axiom because Coq doesn't have an extensional equality. In some sense this proof is incomplete, because there are other classical atomic formulas other than equality on natural numbers. However this does cover all of classical higher order arithmetic, which is probably enough to illustrate my point. Require Import Eqdep_dec. Require Import Logic.FunctionalExtensionality. Inductive IsClassic : Prop -> Type (* could, in principle, be Prop -> Prop *) := | isTrue : IsClassic True | isFalse : IsClassic False | isNatEq : forall n m:nat, IsClassic (n = m) | isAnd : forall A B, IsClassic A -> IsClassic B -> IsClassic (A/\B) | isImpl : forall A B, IsClassic B -> IsClassic (A -> B) | isForall : forall A B, (forall a:A, IsClassic (B a)) -> IsClassic (forall a:A, B a). Lemma ClassicProofIrrelevent : forall P, IsClassic P -> forall p q : P, p = q. Proof. intros P. induction 1. intros [] []; reflexivity. intros []. intros p; generalize p. rewrite p; clear p. intros p. apply K_dec_set. decide equality. symmetry. apply K_dec_set. decide equality. reflexivity. intros [p0 p1] [q0 q1]. rewrite (IHX1 p0 q0), (IHX2 p1 q1). reflexivity. auto using @functional_extensionality_dep. auto using @functional_extensionality_dep. Qed. (1 Comment |Comment on this)
Sunday, December 28th, 2008
11:14 pm	Reader Applicative Functor I was conjecturing that the applicative functor interface to the reader monad was nice to work with because the reader monad is a commutative monad. However, Saizan suggested it was more than that. One key function that the applicative interface cannot define is miffy (from Conor's paper) where miffy :: Monad m => m Bool -> m a -> m a -> m a miffy mb mx my = do b <- mb if b then mx else my The best that the applicative functor can define is iffy where iffy = liftA3 (\b x y -> if b then x else y) The problem is that iffy always runs the "effects" of the applicative functor for both branches of the "if" statement. Thus iffy (Just True) (Just ()) Nothing reduces to Nothing while miffy (Just True) (Just ()) Nothing is Just (). The reader monad enjoys the property that miffy is equivalent to iffy, so nothing is lost here by using the applicative functor interface. This is probably the reason that the applicative functor interface to our step function monad is so pleasant to work with. (Comment on this)
Monday, October 27th, 2008
2:14 pm	Dependent Fixpoints I (more or less) had a function of type Q -> Q -> ... -> Q (more specifically of type n_Function Q Q n) that I wanted to lift to type Q --> Q --> ... --> Q (more specifically of type n_UnifromlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n). This involves proving at each level that the function is uniformly continuous, and then wrapping that proof up into the uniformlyContinuousFunction structure. The natural way to try to do this is something like: Fixpoint MVP_u n : MultivariatePolynomial Q_as_CRing n -> n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n. match n return MultivariatePolynomial Q_as_CRing n -> n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n with | O => fun p => p | S n' => fun p => Build_UniformlyContinuousFunction (fun x => MVP_u n' (p!x)) (MVP_modulus p) ??? end. The problem is that ??? must prove that fun x => MVP_u n' (p!x) is uniformly continuous, but MVP_u is the recursive call. We want to know that MVP_u is our interpretation of p, but all we know is its type. We cannot reduce recursive calls in fixpoints when defining the fixpoint. I found no other way to deal with this problem other than by using a sigma type for my fixpoint result type that contains a proof that the resulting function is what I expect. Fixpoint MVP_uc_sig (n:nat) : MultivariatePolynomial Q_as_CRing n -> n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n -> Type := match n return MultivariatePolynomial Q_as_CRing n -> n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n -> Type with | O => fun p x => p==x | (S n') => fun p f => forall v, MVP_uc_sig n' (p ! v) (f v) end. Fixpoint MVP_uc n : forall (p:MultivariatePolynomial Q_as_CRing n), {f:n_UniformlyContinuousFunction Q_as_MetricSpace Q_as_MetricSpace n |MVP_uc_sig _ p f} := ... (Comment on this)
Thursday, September 25th, 2008
8:59 pm	How to fight Cofixpoint guards Vas asks the question, how come the following doesn't satisfy the guardedness condition? Set Implicit Arguments. CoInductive LList (A:Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. Implicit Arguments LNil [A]. CoFixpoint append (A:Set) (l1 l2 : LList A) : LList A := match l1 with | LNil => l2 | LCons x xs => LCons x (append xs l2) end. CoFixpoint cycle (A:Set) (input : LList A) : LList A := match input with | LNil => LNil | LCons x xs => LCons x (append xs (cycle input)) (* "unguarded recursive call" *) end. The problems with this is that Coq is concerned that append will do something nasty like consume some constructors. If it did then cycle would not be productive. The first solution I came up with was to inline append and simplify. That worked, but I didn't understand why Coq wasn't doing that in the original code. Coq will do reduction when checking the guardedness condition. The problem was that my simplifications was neither β nor ι reduction. I was substituting parametric parameters into the definition of append. If we make the parametric parameters actual function parameters, then Coq will be able to do this substitution by β reduction. One small problem is that A and l2 are the parametric parameters, and we will need to reorder the parameters so that all the parametric ones come first. However, a little notation will allow us to write the parameters in a natural order. Set Implicit Arguments. CoInductive LList (A:Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. Implicit Arguments LNil [A]. Section Append. Variable A:Set. Variable l2:LList A. CoFixpoint append0 l1 : LList A := match l1 with | LNil => l2 | LCons x xs => LCons x (append0 xs) end. End Append. Notation "'append' l1 l2" := (append0 l2 l1) (at level 0, l1 at level 0, l2 at level 0). CoFixpoint cycle (A:Set) (input : LList A) : LList A := match input with | LNil => LNil | LCons x xs => LCons x (append xs (cycle input)) end. I'm not an expert on parsing levels, but setting everything to level 0 seems to work in the few cases I've tried. Defining an infix notation is probably more reasonable for append anyways. (Comment on this)
Monday, September 22nd, 2008
8:20 pm	Mistake found in Lemma cpoly_C_. Lemma cpoly_C_ : forall c : R[x], _C_ c [=] c[+X*]0. algebra. Qed. has a mistake in it. The statement ought to read forall c : R, _C_ c [=] c[+X*]0. It is no problem to fix it. I only point this out because it is interesting to find mistakes in computer verified theorems. No one directly uses this lemma (but it is part of a hint database), so no one noticed this mistake before. (1 Comment |Comment on this)
Wednesday, June 4th, 2008
2:19 pm	Reasoning About Ap Using Setoids. Our current implementation of step functions in Coq makes use of them as an applicative functor. This means that we run into issues about reasoning extensional when dealing with step functions of functions, StepF (X -> Y). Our current methods works requires a setoid record structure, and thus we actually work with StepFS (X --> Y) where --> constructs a setoid of respectful functions (aka Morphisms) between setoids X and Y. However, this is a little clumsy to use because one cannot use a function f : X -> Y directly. Instead, one always needs to define a new function fS : X --> Y by pairing f with its proof of respect. Recently I've been working with mattamresearch to see if I can use his new setoid/type-class mechanism instead. The new setoid system supports higher-order morphisms. Thus one can say that map f is a morphism whenever f is a morphism. This is done by declaring map as a morphism with signature (Xeq ==> Yeq) ==> StepF_eq Xeq ==> StepF_eq Yeq. Attempt 1 was to define an equivalence relation StepF_eq Xeq on StepF X for any equivalence relation Xeq. This worked fairly well until we get to trying to declare Ap to be a morphism with signature StepF_eq (Xeq ==> Yeq) ==> StepF_eq Xeq ==> StepF_eq Yeq. The problem is that (Xeq ==> Yeq) is a PER, and not an equivalence relation, so it cannot be passed as an argument. This attempt failed. Attempt 2 was to define a default relation StepF_eq Xeq on StepF X for any default relation Xeq. Then we can declare that StepF_eq Xeq is an equivalence relation whenever Xeq is an equivalence relation. Now the signature for Ap is no problem because StepF_eq will construct a relation out of any relation, including a PER. I haven't completed my proof that Ap is a morphism, but I have gotten it to the point where I'm fairly convinced I could do it. But I still wondered, even if I prove it is a morphism with the above signature, will I be able to effectively use it? So I Admitted the proof and tried it out on the first lemma: f <@> (glue o l r) == glue o ((SplitL f o) <@> l) ((SplitR f o) <@> r) (where <@> is infix Ap). The first task is to replace the f on the left with (glue o (SplitL f o) (SplitR f o)). The lemma sating that StepF_eq Zeq z (glue o (SplitL z o) (SplitR z o)) requires that Zeq be an equivalence relation. However, f has type StepF (X->Y) and the default relation on (X -> Y) is only a PER. I have a new idea to tackle this problem. The theorem StepF_eq Zeq z (glue o (SplitL z o) (SplitR z o)) can be strengthened to StepF_eq eq z (glue o (SplitL z o) (SplitR z o)). This may appear to be a silly thing to do, but it has a significant effect on the Ap morphism. The Ap morphism works for all equivalence relations Xeq and Yeq. In particular the signature StepF_eq (eq ==> Yeq) ==> StepF_eq eq ==> StepF_eq Yeq is a valid instance, but has the benefit that (eq ==> Yeq) is an equivalence relation. So I think I can rewrite f using the equivalence relation (eq ==> Yeq). The tricky bit is deciding the best way of coxing the rewrite mechanism to use this relation. I'll give this a try, but I'm starting to feel like this is turning into a research topic, rather than a drop in replacement for our existing system. I don't want to turn a little clumsy system into a more clumsy system. (1 Comment |Comment on this)
Monday, April 7th, 2008
12:01 pm	How can I share real number expression (keeping the best approximation)? My recommendation is to arrange one's formulas so that expressions are evaluated at most once. One would like a way of combining n-functions that (that will be applied to a common expression) into one function that uses the finest approximation of them all. I think some higher order combinators (+ on functions) may help a lot for this; but it may not be possible to ensure that expression are evaluated at most once in general. This is because some approximations are used to determine how much to approximate other values. For example in x*y, the approximation of x is used to determine how much to approximate y. So there doesn't seem to be a way of generically sharing the x's in x*x. Of course, there is is perhaps always a specific way to do sharing: in this case use x^2 instead. (Comment on this)
Tuesday, March 4th, 2008
10:26 pm	IO and m-sets I understand an M-set(oid) to be a dependent record type containing a carrier setoid, an M-action on that carrier, and then a proof that the action really is a monoid action. Roughly speaking, Record (M:Monoid) MSetoid : { car : Setoid act : M -> car -> car pf1 : forall x, act 1 x == x pf2 : forall a b x, act (a*b) x == act a (act b x) } A morphism between two MSetoids is a homomorphism: Record (M:Monoid)(X Y:MSetoid M) : Mmorphism : { f : car X --> car Y (* preserves setoid *) pf : forall a x, act a (f x) == f (act a x) } The idea is to see IO in terms of a particular M-set. In GHC, IO a is defined to be RealWorld -> a * RealWorld. This is isomorphic to (RealWorld -> a)*(RealWorld -> RealWorld). The idea is that this is the same as (car IOMS*(Endo RealWorld), where car IOMS is RealWorld -> a, and act IOMS is (fun a x rw => x (a rw)). To get us started let us take an unstructured approach and consider RealWorld to be the Baire space Stream nat. Actually, I will use the isomorphic structure (Stream nat)*(Stream nat). Some example semantics. putChar : nat -> (RealWorld -> ())*(RealWorld -> RealWorld) putChar n = (fun _ ==> (), fun (i,o) => (i,n:o)) getChar : (RealWorld -> nat)*(RealWorld -> RealWorld) getChar = (fun (i,_) ==> hd i, fun (i,o) => tl (i,o)) I have no idea why we want to see IO in terms of M-sets, or if this is even right. (1 Comment |Comment on this)
Wednesday, February 6th, 2008
2:59 pm	Are the Constructive Real the same as the Classical Reals The constructive reals are functions (sequences) paired with a proof that the sequences are Cauchy. The classic reals are relations (predicates) that have the (classical) function property, again paired with a proof that the sequence is Cauchy. From the world we live in, we see that the constructive reals are a subset of the classical reals. Both sets are countable from our point of view. Both sets consist of lambda expressions. There is an injection from the constructive reals to the classical reals. But we see that there are some classical reals that for which we are sure there is no corresponding lambda expression in the constructive reals. From the world inside Coq, both sets are uncountable. Coq is agnostic about whether the constructive and classical reals are the same. It sees the injection from the constructive reals to the classic reals, but it doesn't see any injection the other way; however, it also doesn't see any classic real that is clearly not in the image of the injection either. From the classical world (inside the constructive world), the constructive reals and classical reals are isomorphic. There is a classical isomorphism (a relation that is a classical bijection) between the two types. An interesting side remark is that from out perspective the countable set that is the reals (constructive or classical) is decidable. Because we require a proof object witnessing the fact that the sequence is Cauchy. This means that there are some functions that are Cauchy but not provably Cauchy. In this interpretation we reject these as real numbers. (Comment on this)
Monday, February 4th, 2008
8:55 pm	Sin Theorem ball (m:=Compact.Compact stableQ2) (308 # 5200) graphCR uc_compose (uc_compose (boundBelow (- (1))) (boundAbove 1)) (uc_compose sin_uc (Qscale_uc 3)) [- (1) .. 1] (Cunit (- (1), 1)⇱ ⎥                 ████    ⎢ ⎥                ██  ██   ⎢ ⎥                █    █   ⎢ ⎥               ██    ██  ⎢ ⎥               █      █  ⎢ ⎥              ██      ██ ⎢ ⎥              █        █ ⎢ ⎥              █        █ ⎢ ⎥             █          █⎢ ⎥             █          █⎢ ⎥             █          █⎢ ⎥            █            ⎢ ⎥            █            ⎢ ⎥            █            ⎢ ⎥█          █             ⎢ ⎥█          █             ⎢ ⎥█          █             ⎢ ⎥ █        █              ⎢ ⎥ █        █              ⎢ ⎥ ██      ██              ⎢ ⎥  █      █               ⎢ ⎥  ██    ██               ⎢ ⎥   █    █                ⎢ ⎥   ██  ██                ⎢ ⎥    ████                 ⎢ ⇲(1, - (1))) (Comment on this)
Friday, February 1st, 2008
11:55 am	Proofs & Programming Having to prove properties (correctness) about functions as you develop them really does catch the corner cases. When programming my compact intervals, there were several boundery case errors that were caught. One task was to find a point a close by point on my nice regular lattice between l and r for any point x∈[l, r]. When x lies directly between two lattice points, then either the point on the left or right is acceptable. I ended up always rounding up; but there was a problem with my code. When x was r it would still round up, and return a lattice point that is outside [l, r]. This needed to be fixed. The other error was when l is r. In that case i determined that the number of lattice points needed was 0. But this is wrong. 1 point is still needed to distinguish it from the empty set. Working around these error cases makes my code less elegant, so perhaps I'm approaching this problem wrong. But in any case it was nice to see proofs catching coding errors. (Comment on this)
Thursday, January 31st, 2008
11:13 am	Solving Inequalities with Partial Functions I cannot rewrite partial functions because setoid rewriting isn't allowed for dependent parameters. One idea I have is to rewrite the dependent parameters into one dependent sum parameter. Then I can put an setoid relation on that dependent sum type, and rewrite it. Perhaps this will work. (Comment on this)
Tuesday, January 29th, 2008
11:49 am	Prelength Space of FinEnum I cannot prove that the space of finitely enumerable sets of X is a prelength space when X is a prelength space without some additional assumption such as X being a located-metric space. One potential solution is to replace the constructive quantifier in the definition of a prelength space with a classical existential quantifier. This would be fine because the prelength property is only used to show that the image of a regular function under a uniformly continuous function is also regular. The actual point generated is not needed for computation. The only catch is that I would then require that balls be stable, and at this point, one might as well add stability to my definition of a metric space. Getting the definitions right to handle these subtle cases is quite difficult because in all my applications my metric spaces are located, so none of these different possible definitions matter. (Comment on this)
Thursday, January 17th, 2008
10:44 am	Complete Complete is Complete One of the monad laws is that join ∘ unit ≍ id. The completion monad also as the law that unit ∘ join ≍ id, which completes the isomorphism between the double completion and single completion of a metric space. (Comment on this)
Friday, January 4th, 2008
7:56 pm	Interpreting Finitely Enumerable Sets When I interpret the completion of finite(ly enumerable) sets as compact sets, I interpret it as a predicate that holds for any point that is within ε of some point in the ε approximation for every ε. Therefore it is only fair that I interpret my finite(ly enumerable) sets themselves as compact sets in the same way. This means that although finitely enumerable sets themselves are not necessarily compact, their interpretation always is. (Comment on this)
3:01 pm	Different Degrees of Finiteness Everyone agrees that a finite set (predicate) is one for which there exists a bijection with Fin n for some n. When there is exists a surjection from Fin n to the set, this is called finitely enumerable or sometimes called subfinite. However, as Erik Palmgren notes, a subset of a finite set could be neither finite, nor finitely enumerable. I need a name for this, and I'm thinking of stealing subfinite for it. Does there already exist a term for being a subset of a finite set? (Comment on this)
Thursday, January 3rd, 2008
2:25 pm	Well-Founded Recursion and Proof Irrelevance Yesterday I had a nice chat with Matthieu about the upcoming Coq release that will have proof irrelevance. Proof irrelevance means that all objects of some proposition are equal (perhaps they are even convertible). The problem with proof irrelevance is that it can screw up fixpoint reduction when you have a proof of termination witnessed by something in Prop. The standard example of this is well-founded recursion where the recursion is over Acc. Well-founded recursion is nice because it does structural recursion over a proposition. When extracting the program the proposition goes away and you are left with just the relevant computational parts. The problem occurs when well founded recursion is done inside an inconsistent context. Then the proof of termination may be based on false premises. If all the different termination proofs happen to be convertible, then the fixpoint can always unfold. Then you lose normalization. What I vaguely understand is that the forthcoming version of Coq will have proof irrelevance. It will give you the choice between reducing these fixpoints and losing strong normalization, or not reducing these fixpoints and losing canonicity. Lack of canonicity would mean that there would be some natural numbers which don't begin with a constructor. Up till now I had figured that Epigram 2 with its OTT logic would have everything I want: proof irrelevance, functional extensional equality, etc. Matthieu asked me what OTT loses. I said that it loses inductive types in Prop, but I figured that was no big deal. Then Matthieu asked me how to do well-founded recursion in OTT. The problem is that Acc is inductively defined. I had assumed that there would be some non-inductive replacement for it, but now it is not looking that way. I believe I was told that all propositions in OTT are double-negation stable. I thought that maybe if I prove that Acc is stable, then I would get some insight into how to define it without induction. The problem is that I cannot prove that Acc is stable. This really surprised me. It is my first example of something that is proof irrelevant (assuming functional extensional equality), but not double negation stable. Matthieu pointed me to the a lemma done by the Chalmers people that stability of Acc implies Markov's principle. I redid this proof in Coq to see the result for myself. Since Markov's principle isn't constructive, we cannot expect Acc to be stable. Since (i believe) that all props in OTT are stable, that means that Acc cannot be defined in Prop in OTT. When squash types are added to OTT, then these new squashed propositions are not double negation stable. One one solution may be to define Acc in Type and then squash it into Prop. But I don't know what the reduction properties would be, or if this would even work. I'm starting to think that the following four things are incompatible Well-founded recursion Proof irrelevance Canonicity Normalization By well-founded recursion, I mean being able to do structural recursion over propositions to product a value in type, such as recursion over Acc (of course if you put Acc in Type then everything works, but we don't want to do that because we want to strip Acc during program extraction). By proof irrelevance I mean that all proofs of the same proposition are equal (and maybe I mean that they are convertible). By canonicity I mean that all normalized inductive objects in the empty context begin with a constructor. Coq currently leaves out proof irrelevance. The forthcoming version of Coq will leave out (at your choice) either canonicity or normalization (as I understand). Finally, OTT leaves out well-founded recursion (as I've defined it). Perhaps OTT plus squash types will give all 4 properties, but I don't think I would bet on it. (Comment on this)
Saturday, December 22nd, 2007
8:14 pm	New Induction Principles I am trying to make more induction principles in Coq. They are incredibly useful. They take advantage of Coq's pretty good second order unification. I've made two nice induction principles recently. The first is a new induction/recursion method for positive binary numbers. Definition positive_rect2 (P : positive -> Type) (c1 : forall p : positive, P (Psucc p) -> P p -> P (xI p)) (c2 : forall p : positive, P p -> P (xO p)) (c3 : P 1%positive) (p : positive) : P p := It is exactly the same as the normal one, but the 2*p + 1 case gives you recursive access to both p and p+1. Of course there are all sorts of nice induction principles one could make for positive, but this one still generates functions that operate in ln(n) time. The second on is just an induction principle. When dealing with induction to prove predicates defined on two partitions, it is often helpful to create a common refined partition and work on that one instead. But I never bothered to make a procedure to make a common refined partition. It just seemed like too much work to juggle the proof obligations that the two partitions had the same refinement. Plus, the details of how my partitions are refined is an intensional property of my step functions defined on the partition, and naturally I prefer to work with properties that respect my equivalence relation. If I had a common refined partition, the next step would be to do induction over that common refinement. This lead to a recent realization that I could come up with an elegant induction principle that captures both the refinement and induction all in one. Lemma StepF_ind2 : forall (X Y : Setoid) (P : StepF X -> StepF Y -> Prop), (forall (s s0 : StepF X) (t t0 : StepF Y), (s==s0) -> (t==t0) -> P s t -> P s0 t0) -> (forall (x:X) (y:Y), P (constStepF x) (constStepF y)) -> (forall (o : OpenUnit) (s s0 : StepF X) (t t0 : StepF Y), P s t -> P s0 t0 -> P (glue o s s0) (glue o t t0)) -> forall (s:StepF X) (t:StepF Y), P s t. This induction principles allows you to do simultaneous induction on two step functions with only two cases to consider. The first case is that both step functions are constant functions. The second case is that both step functions are two step functions that are glued together at the same point. So the user gets the impression that the two step functions share a common partition. The only catch is that you need to prove that the predicate respects the equivalence relation on step functions. But 80% of the time the predicate is composed out of functions that respect this equivalence relation. The main exception is when proving that a new definition is well defined with respect to this equivalence relation and there is no escaping intensional reasoning in that case. Another nice thing about this induction principle was that it was simple to prove. Proof. intros X Y P wd c0 c1. induction s using StepF_ind. induction t using StepF_ind. apply c0. apply wd with (s:=(glue o (constStepF x) (constStepF x))) (t:=glue o t1 t2); try reflexivity. apply (glueSplit (constStepF x) o). apply c1; assumption. intros t. eapply wd. reflexivity. apply glueSplit with (a:=o). apply c1; auto. Qed. This basically captured a proof pattern that I had been repeating over and over. I only wish I had invented this induction principle sooner. (Comment on this)
Thursday, December 20th, 2007
7:59 pm	Integration using Monads Integration is a combination of limits and step functions. We implement it as a combination of the completion monad, for limits, and the step function monad. A step function on [0, 1] (or just step function for short) is either a constant, or two step functions squished and glued together at a rational point in ]0, 1[. Step functions are not really functions because we define no evaluation method for it. This allows us to avoid concerns about how it is defined at the jump discontinuities. Although the step functions form a monad, we just implement the functions and laws for an applicative functor. The step functions to ℚ form a metric space in several ways. Two particular ways are the using the L1 and L∞ norms. Completing the step functions to ℚ with respect to the L1 norm yields what I call the integrable functions. Again integrable functions are not really functions. Even if there was an evaluation method, it wouldn't respect the equivalence relation on the metric space. However we can integrate integrable functions. Riemann integration (on [0,1]) is now straight forward. Approximate a uniformly continuous function (from ℚ to ℝ) as a step function by sampling it uniformly between 0 and 1. Then take the limit of these step functions to get its representation as an integrable function. When trying to prove that this sequence of approximations of step functions converges, it struck me that the continuous function is effectively being mapped over a monotonic step function of sample points. Therefore it made sense to separate integration into two pieces. First take the limit of a series of uniform monotonically increasing step functions on [0, 1]. This series is more easily seen to converge. I name the limit id01, which is the integrable function representing the identity function on [0, 1]. Then as a second step is to map the function to be integrated over id01. This is done by first showing that map f produces a uniformly continuous function from (step functions to ℚ) to (step functions to ℝ). The step function monad distributes over the completion monad. This yields an embedding from (step functions to ℝ) to integrable functions. Now distrb . (map f) is a uniformly continuous function from (step functions to ℚ) into integrable functions. Finally we bind this to id01 using bind from the completion monad. bind (distrb . (map f)) id01 is f as an integrable function. This can then be integrated. This may seem like a complicated way of integrating, but it really is exactly the same as Riemann integration. Breaking the problem into several steps has made the problem easier to reason about, and allowed us to reuse the theory of distributive monads to tackle the problem. It also opens integration up to some interesting tinkering. The choice of binding to id01 is clearly correct, but any integrable function could go in place of id01. What would happen if we replaced that with another integrable function? It turns out changing this yields the Riemann-Stieltjes integral. Specifically we can compute the Riemann-Stieltjes ∫[0, 1] f dg for a cumulative distribution function g, by binding to g−1 instead of id01. Because g−1 is only required to be an integrable function, it can be non-continuous. It is then easy to integrate with respect to measures that are not absolutely continuous with respect to the Lebesgue measure. In particular when we bind to the constant step function a, the result of integration yields f(a). Thus integration with respect any Dirac delta measure is a breeze. In conclusion, our quest implement Riemann integration with formal proofs by breaking the problem into manageable components has naturally lead us down a path to that yielded the more general Riemann-Stieltjes integral. (1 Comment |Comment on this)
Friday, November 2nd, 2007
10:35 am	Old bug in Haskell code I had a bug in my original Haskell program. The original idea was that I would restrict x−1 to a domain where it is uniformly continuous, such as [c, ∞) for 0 < c. So if x was a real number greater than c, I assumed everything would work out. The problem was that even though x may be a real number greater than c, an approximation to x may be less than c. I noticed this bug when I got a division by 0 error. Due to compression, sometimes my approximation of x was 0 for a sufficiently large approximations. This lead to division by 0 errors in my Haskell code. The solution was to inject x into the completion of [c, ∞), so that all its approximations are in [c, ∞), or equivalently consider the total function (max c x)−1 instead. (Comment on this)