[ Content | View menu ]

Research Blog

“General Recursion using Coinductive Monad” Got Right

October 2, 2008

Anton Setzer argued in his letter to the Agda mailing list that we should go back to a category theoretical view of codata, and Dan Doel soon successfully experimented the ideas.

[More ...] - 0 Comments
Tags: , , .

General Recursion using Coindutive Monad

September 28, 2008

It would be nice to if we could write the program and prove its termination separately. Adam Megacz published an interesting paper: A Coinductive Monad for Prop-Bounded Recursion. As a practice, I tried to port his code to Agda.

[More ...] - 0 Comments
Tags: , , .

Typed λ Calculus Interpreter in Agda

September 24, 2008

In a recent meeting I talked to my assistants about using dependent type to guarantee that, in an evaluator for λ calculus using de Bruin indices, that variable look-up always succeeds.

[More ...] - 0 Comments
Tags: , , .

Tail-Recursive, Linear-Time Fibonacci

July 12, 2008

How can I introduce accumulating parameters to derive the linear-time, tail recursive implementation of fib.

[More ...] - 2 Comments
Tags: , .

A Simple Exercise using the Modular Law

May 27, 2008

Prove the following property in point-free style:

S ⊆ C . S     ⇐     R ⊆ C . R   ∧   S ⊆ R

[More ...] - 0 Comments
Tags: .

Well-Foundedness and Reductivity

April 25, 2008

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.

[More ...] - 0 Comments
Tags: , , , .

Well-Founded Recursion and Accessibility

April 20, 2008

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.

[More ...] - 2 Comments
Tags: , , .

Terminating Unfolds (2)

April 13, 2008

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.

[More ...] - 0 Comments
Tags: , , .

Terminating Unfolds (1)

April 8, 2008

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

[More ...] - 0 Comments
Tags: , , .

Constructing List Homomorphism from Left and Right Folds

February 10, 2008

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 .

[More ...] - 1 Comments
Tags: , .