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

Skip to content
# Agda

## Well-Foundedness and Reductivity

## Well-Founded Recursion and Accessibility

## Terminating Unfolds (2)

## Terminating Unfolds (1)

## AoPA — Algebra of Programming in Agda

## Maximum Segment Sum, Agda Approved

## Agda Exercise: Proving that Mergesort Returns Ordered Lists

## Agda Exercise: Sized Mergesort

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

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.

Given a relation

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

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

The **AoPA** library allows one to encode Algebra of Programming style program derivation, both functional and relational, in Agda, accompanying the paper Algebra of Programming Using Dependent Types (MPC 2008) developed in co-operation with Hsiang-Shang Ko and Patrik Jansson.

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…

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.

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`

.

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.