Tag Archives: Optimisation Problems

A “Side-Swapping” Lemma Regarding Minimum, Using Enriched Indirect Equality

If every solution returned by D is no better than some solution returned by X, any optimal solution by X must be no worse than some optimal solution by D “What? How could this be true?” It turned out that the reasoning can be correct, and the proof uses indirect equality in an unusual way.

Posted in Research Blog | Also tagged , | Leave a comment

The Windowing Technique for Longest Segment Problems

Reviewing Zantema’s “windowing” technique for computing the longest segment of the input that satisfies a suffix-closed predicate.

Posted in Research Blog | Also tagged , | Leave a comment

Longest Segment Satisfying Suffix and Overlap-Closed Predicates

Translating Zantema’s work to Bird-Meertens style, to compute the longest consecutive segment of the input that satisfies a predicate that is suffix and overlap-closed.

Posted in Research Blog | Also tagged , | Leave a comment

On a Basic Property for the Longest Prefix Problem

Giving a constructive proof for one of the essential properties in Hans Zantema’s Longest Segment Problems.

Posted in Research Blog | Also tagged , | Leave a comment

Algebra of programming in Agda: dependent types for relational program derivation

S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming in Agda: dependent types for relational program derivation. In Journal of Functional Programming, Vol. 19(5), pp. 545-579. Sep. 2009. [PDF]

Posted in Journal | Also tagged , , | Leave a comment

AoPA — Algebra of Programming in Agda

The AoPA library allows one to encode Algebra of Programming style program derivation, both functional and relational, in Agda, accompanying the paper Algebra of Programming Using Dependent Types (MPC 2008) developed in co-operation with Hsiang-Shang Ko and Patrik Jansson.

Posted in Software | Also tagged , , | Leave a comment

Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths

S-C. Mu. Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths. In Partial Evaluation and Program Manipulation (PEPM ’08), pp 31-39. January 2008.
[PDF] [GZipped Postscript]

Posted in Conference | Also tagged , | Leave a comment

Maximum Segment Sum, Agda Approved

To practise using the Logic.ChainReasoning module in Agda, Josh proved the foldr-fusion theorem, and I thought it would be an small exercise over the weekend to start off where he finished…

Posted in Research Blog | Also tagged , , | 2 Comments

The Pruning Theorem: Thinning Based on a Loose Notion of Monotonicity

Any preorder R induces a lax preorder ∋ . R. If a relation S is monotonic on R∘, it is monotonic on lax preorder ∋ . R. Furthermore, prune (∋ . R) = thin R. Therefore, pruning is a generalisation of thinning. We need the notion of lax preorders because, for some problems, the generating relation S is monotonic on a lax preorder, but not a preorder.

Posted in Research Blog | Also tagged , | Leave a comment

Proving the Thinning Theorem by Fold Fusion

Prove the thinning theorem by fold fusion. Horrifyingly, I could not do it anymore! Have my skills become rusty due to lack of practice in the past few years?

Posted in Research Blog | Also tagged , | Leave a comment