Category Archives: Research Blog

The Windowing Technique for Longest Segment Problems

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

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

Longest Segment Satisfying Suffix and Overlap-Closed Predicates

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.

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

On a Basic Property for the Longest Prefix Problem

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

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

No Inverses for Injective but Non-Surjective Functions?

“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?

Posted in Research Blog | Tagged , , | 12 Comments

Proof Irrelevance, Extensional Equality, and the Excluded Middle

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.

Posted in Research Blog | Tagged , | 7 Comments

“General Recursion using Coinductive Monad” Got Right

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.

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

General Recursion using Coindutive Monad

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.

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

Typed λ Calculus Interpreter in Agda

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.

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

Tail-Recursive, Linear-Time Fibonacci

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

Posted in Research Blog | Tagged , | 2 Comments

A Simple Exercise using the Modular Law

Prove the following property in point-free style:

S ⊆ C . S     ⇐     R ⊆ C . R   ∧   S ⊆ R
Posted in Research Blog | Tagged | Leave a comment