# Agda

## 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.

## 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.

## 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.

## 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.

## 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…

## Agda Exercise: Sized Mergesort

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`.

## My First Agda Program: Append, Reverse, and Merge

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.