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…
Research Blog
The Pruning Theorem: Thinning Based on a Loose Notion of Monotonicity
Any preorder
Proving the Thinning Theorem by Fold Fusion
Prove the thinning theorem by fold fusion. Horrifyingly, I could not do it anymore! Have my skills become rusty due to lack of practice in the past few years?
Agda Exercise: Proving that Mergesort Returns Ordered Lists
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.
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.
An Unsuccessful Attempt to Compute the Intersection of Regular Expressions
Tyng-Ruey, Chin-Lung, and I needed to compute the intersection of two regular expressions without converting them to finite automata. The result was not satisfactory, however.
Developing Programs and Proofs Spontaneously using GADT
I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language. I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna’s introduction to Epigram: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one.
Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus
An indcutive type μF is simulated by forall x . (F x -> x) -> x, while a coinductive type νF is simulatd by exists x . (x -> F x, x). When they coincide, we can build hylomorphisms, but also introduces non-termination into the language.
Proving Some Equalities in Propositional Logic
Proving De Morgan’s laws and the double negation law in boolean algebra. Notes taken while listening to Max’s course on logic.