## A Survey of Binary Search

If you think you know everything you need to know about binary search, but have not read Netty van Gasteren and Wim Feijen’s note The Binary Search Revisited, you should.

Skip to content
# Research Blog

## A Survey of Binary Search

## A “Side-Swapping” Lemma Regarding Minimum, Using Enriched Indirect Equality

## Determining List Steepness in a Homomorphism

## The Windowing Technique for Longest Segment Problems

## Longest Segment Satisfying Suffix and Overlap-Closed Predicates

## On a Basic Property for the Longest Prefix Problem

## No Inverses for Injective but Non-Surjective Functions?

## Proof Irrelevance, Extensional Equality, and the Excluded Middle

## “General Recursion using Coinductive Monad” Got Right

## General Recursion using Coindutive Monad

If you think you know everything you need to know about binary search, but have not read Netty van Gasteren and Wim Feijen’s note The Binary Search Revisited, you should.

If every solution returned by `D`

is no better than some solution returned by `X`

, any optimal solution by `X`

must be no worse than some optimal solution by `D`

“What? How could this be true?” It turned out that the reasoning can be correct, and the proof uses indirect equality in an unusual way.

A list of numbers is called *steep* if each element is larger than the sum of elements to its right. It is an example we often use when we talk about tupling. Can we determine the steepness of a list by a list homomorphism?

Reviewing Zantema’s “windowing” technique for computing the longest segment of the input that satisfies a suffix-closed predicate.

Translating Zantema’s work to Bird-Meertens style, to compute the longest consecutive segment of the input that satisfies a predicate that is suffix and overlap-closed.

Giving a constructive proof for one of the essential properties in Hans Zantema’s Longest Segment Problems.

“I cannot prove that if a function is injective, it has an inverse,” Hideki Hashimoto posed this question to me. Is it possible at all?

I was puzzled by the fact stated in a number of places that axiom of choice, proof irrelevance, and extensional equality together entail the law of excluded middle.

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.

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.