December 5, 2007
By chance, I came upon a blog entry by Masahiro Sakai (酒井政裕) in which he, after reading my short comment “Do you know that the S combinator is injective?”, tried to construct the inverse of S and showed that S⁻¹ ○ S = id in, guess what, Agda!
[More ...]
- 7 Comments
Tags: Program Inversion, λ calculus.
November 26, 2007
Given an interpreter of a small language, derive a virtual machine and a corresponding compiler
[More ...]
- 5 Comments
Tags: Program Derivation.
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…
[More ...]
- 2 Comments
Tags: Agda, Program Derivation, Segment Problems.
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.
[More ...]
- 0 Comments
Tags: Program Derivation, Thinning Theorem.
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?
[More ...]
- 0 Comments
Tags: Program Derivation, Thinning Theorem.
September 28, 2007
This time I am implementing the example in another section of Why Dependent Types Matter by Altenkirch, McBride, and McKinna in Agda: proving that mergesort returns an ordered list.
[More ...]
- 2 Comments
Tags: Agda, Dependent Type.
September 27, 2007
Continuing with my Adga programming practice. Part of the mergesort example became easy once Max showed me how I should perform the pattern matching in insert.
[More ...]
- 4 Comments
Tags: Agda, Dependent Type.
September 19, 2007
During the WG 2.1 meeting, my attention was brought to Agda. So, here is my first Agda program. I am merely repeating some simple exercises on lists, which I tried using Haskell in a previous entry Developing Programs and Proofs Spontaneously using GADT.
[More ...]
- 2 Comments
Tags: Agda, Curry-Howard, Dependent Type.
August 9, 2007
Tyng-Ruey, Chin-Lung, and I needed to compute the intersection of two regular expressions without converting them to finite automata. The result was not satisfactory, however.
[More ...]
- 2 Comments
Tags: Regular Expression.
August 6, 2007
I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language. I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna’s introduction to Epigram: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one.
[More ...]
- 3 Comments
Tags: Curry-Howard, Dependent Type, GADT, Haskell, Types.