http://www.iis.sinica.edu.tw/~scm Research Blog of 穆信成 Shin-Cheng Mu Wed, 23 Jul 2008 03:54:06 +0000 http://backend.userland.com/rss092 en For two consecutive years I have been responsible for teaching the program derivation course in the FLOLAC summer school. It was an exam question last year to derive a linear-time solution computing the Fibonacci function, whose definition we all know very well: fib 0 = 0 fib 1 ... http://www.iis.sinica.edu.tw/~scm/2008/tail-recursive-linear-time-fibonacci/ S-C. Mu, H-S. Ko, and P. Jansson. In Mathematics of Program Construction 2008, LNCS 5133, pp 268-283. July 2008. [PDF] Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On the other hand, squiggolists ... http://www.iis.sinica.edu.tw/~scm/2008/algebra-of-programming-using-dependent-types/ Z. Hu, S-C. Mu and M. Takeichi. Higher-Order and Symbolic Computation, Vol 21(1-2), pp 89-118, May 2008.[PDF] This paper presents an application of bidirectional transformations to design and implementation of a novel editor supporting interactive refinement in the development of structured documents. The user performs a sequence of editing operations on ... http://www.iis.sinica.edu.tw/~scm/2008/a-programmable-editor-for-developing-structured-documents-based-on-bidirectional-transformations-2/ Josh needs a property for which there is an obvious pointwise proof. He wonders whether it is possible to prove it in point-free style. I haven't practised point-free proofs for a while, so I'd give it a try. The actual property he needs is that FT . C ⊆ C . ... http://www.iis.sinica.edu.tw/~scm/2008/a-simple-exercise-using-the-modular-law/ Before learning dependent types, all I knew about program termination was from the work of Henk Doornbos and Roland Backhouse [DB95, DB96]. I am curious about the connection between their formulation of well-foundedness by relational calculation and the type theoretic view. It is generally accepted that a relation _<_ is well-founded ... http://www.iis.sinica.edu.tw/~scm/2008/well-foundedness-and-reductivity/ Since Nils Anders Danielsson showed me how to use Induction.WellFounded in Agda's Standard Library, I have been studying issues related to well-founded recursion. In dependently typed programming, we would like to ensure that proof terms are terminating. Apart from the type checker, Agda employs a separate termination checker. How ... http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibility/ After seeing our code, Nils Anders Danielsson suggested two improvements. Firstly, to wrap the bound in the seed. The terminating unfoldr↓ would thus have a simpler type as well as a simpler implemenation: unfoldr↓ : {a : Set}(b : ℕ -> Set){n : ℕ} ->     (f : forall {i} -> b (suc ... http://www.iis.sinica.edu.tw/~scm/2008/terminating-unfolds-2/ The AoPA(Algebra of Programming in Agda) library allows one to derive programs in a style resembling that in the book Algebra of Programming in Agda. For example, the following is a derivation of insertion sort: sort-der : ∃ ([ Val ] -> [ Val ]) (\f -> ordered? ○ permute ⊒ ... http://www.iis.sinica.edu.tw/~scm/2008/terminating-unfolds-1/ An Agda library accompanying the paper Algebra of Programming Using Dependent Types (MPC 2008) developed in co-operation with Hsiang-Shang Ko and Patrik Jansson. Dependent type theory is rich enough to express that a program satisfies an input/output relational specification, but it could be hard to construct the proof term. On ... http://www.iis.sinica.edu.tw/~scm/2008/aopa/ Since Josh has already mentioned it, I had better give it a full account. Back in 2003 when I just started my postdoc in PSD Lab in University of Tokyo, my colleagues there were discussing about the third homomorphism theorem. The theorem says that if a function f can be expressed ... http://www.iis.sinica.edu.tw/~scm/2008/constructing-list-homomorphism/