Category Archives: Research Blog

Well-Foundedness and Reductivity

It seems that reductivity of Doornbos and Backhouse is in fact accessibility, which is often taken by type theorists to be an alternative definition of well-foundedness.

Posted in Research Blog | Tagged , , , | Leave a comment

Well-Founded Recursion and Accessibility

Given a relation < that has been shown to be well-founded, we know that a recursively defined function is terminating if its arguments becomes “smaller” with respect to < at each recursive call. We can encode such well-founded recursion in Agda’s style of structural recusion.

Posted in Research Blog | Tagged , , | 2 Comments

Terminating Unfolds (2)

After seeing our code, Nils Anders Danielsson suggested two improvements. Firstly, to wrap the bound in the seed. Secondly, to define unfoldT↓ using well-founded recursion.

Posted in Research Blog | Tagged , , | Leave a comment

Terminating Unfolds (1)

I hope to come up with a variation of unfoldr which, given a proof of well-foundedness, somehow passes the termination check.

Posted in Research Blog | Tagged , , | Leave a comment

Constructing List Homomorphism from Left and Right Folds

Back in 2003, my colleagues there were discussing about the third homomorphism theorem — if a function f can be expressed both as a foldr and a foldl, there exists some associative binary operator such that f can be computed from the middle. The aim was to automatically construct .

Posted in Research Blog | Tagged , , | 1 Comment

S Combinator is Injective, with Proofs

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!

Posted in Research Blog | Tagged , | 8 Comments

Deriving a Virtual Machine

Given an interpreter of a small language, derive a virtual machine and a corresponding compiler

Posted in Research Blog | Tagged | 5 Comments

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 | 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 | 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 | Tagged , , | Leave a comment