By Shin | Published: February 13, 2010
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.
By Shin | Published: June 20, 2009
Reviewing Zantema’s “windowing” technique for computing the longest segment of the input that satisfies a suffix-closed predicate.
By Shin | Published: June 7, 2009
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.
By Shin | Published: June 2, 2009
Giving a constructive proof for one of the essential properties in Hans Zantema’s Longest Segment Problems.
By Shin | Published: January 31, 2009
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]
By Shin | Published: March 30, 2008
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.
By Shin | Published: November 13, 2007
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]
By Shin | Published: November 11, 2007
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…
By Shin | Published: October 8, 2007
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.
By Shin | Published: October 4, 2007
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?