[Agda] recursion, lexicographic ordering

[Siek, Jeremy]

Dear Matthew,

Thank you so much!

I now have a terminating implementation of
Martello and Montanari’s classic unification algorithm.

This is for a graduate course in programming languages at Indiana University
based on PLFA:
https://jsiek.github.io/B522-PL-Foundations/

Cheers,
Jeremy


On Feb 29, 2020, at 4:07 AM, Matthew Daggitt <matthewdaggitt at gmail.com<mailto:matthewdaggitt at gmail.com>> wrote:

Hi Jeremy,
 Okay, I've written out an example of how you'd use the WellFounded part of the standard library to prove termination below. I haven't gone into the fine details of how `Acc` and `WellFounded` work as there's plenty of excellent resources out there already, e.g. here<https://stackoverflow.com/questions/19642921/assisting-agdas-termination-checker>.

Note that the latest official version of the standard library (v1.2) is missing the proof `×-wellFounded` in `Data.Product.Relation.Binary.Lex.Strict`, as I've just added it to the `lexicographic-product<https://github.com/agda/agda-stdlib/pull/1094>` branch. The proof will however be available in the upcoming v1.3 release.

In the meantime I think the easiest way for you to solve this problem is to copy the updated file<https://raw.githubusercontent.com/agda/agda-stdlib/03209af78061fdf734521359985c9de836e063b8/src/Data/Product/Relation/Binary/Lex/Strict.agda> into your own library and give it a new name such as `MyStrictLexProduct.agda` and import that instead of `Data.Product.Relation.Binary.Lex.Strict`. You can then delete it and switch back when v1.3 releases.

```agda
module Test where

open import Data.Nat
open import Data.Nat.Induction using (Acc; acc; <-wellFounded)
open import Data.Nat.Properties using (≤-refl)
open import Data.Sum using (inj₁; inj₂)
open import Data.Product
open import Data.Product.Relation.Binary.Lex.Strict
open import Induction.WellFounded using (WellFounded)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- Define the order over the 3-tuples using two applications of `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict`:

_<₃_ : Rel (ℕ × ℕ × ℕ) _
_<₃_ = ×-Lex _≡_ _<_ (×-Lex _≡_ _<_ _<_)

-- Use the new `×-wellFounded` combinator to prove that the lexicographic ordering is well-founded:

<₃-wellFounded : WellFounded _<₃_
<₃-wellFounded = ×-wellFounded <-wellFounded (×-wellFounded <-wellFounded <-wellFounded)

-- The naive implementation of this function fails to pass the termination checker
{-
-- BAD: termination checking failure
f : ℕ × ℕ × ℕ → ℕ
f (x , zero  , z) = z
f (x , suc y , z) = f (x , y , suc z)
-}

-- Define a new function that takes in a decreasing Acc proof as well, and hence is acceptable to the termination checker

f-acc : ∀ (x : ℕ) → Acc _<₃_ x → ℕ
f-acc (x , zero  , z) rec       = z
f-acc (x , suc y , z) (acc rec) = f-acc (x , y , suc z)
  (rec _ (inj₂ (refl , inj₁ ≤-refl)))  -- proof that the tuple is decreasing lexicographically

-- Use <₃-wellFounded to provide the Acc proof
f : ℕ × ℕ × ℕ → ℕ
f xyz = f-acc xyz (<₃-wellFounded xyz)
```

Best,
Matthew

On Sat, Feb 29, 2020 at 4:08 PM Matthew Daggitt <matthewdaggitt at gmail.com<mailto:matthewdaggitt at gmail.com>> wrote:
Hi Jeremy,
 So I've been meaning to get rid of `Induction.WellFounded.Lexicographic` for a while as it doesn't mesh with the rest of the library very well. Your question might actually provide me the impetus to do so!

Give me a few hours to upload a new branch to the standard library with some small changes and I'll get back to you with the best way to do so.
Best,
Matthew


On Sat, Feb 29, 2020 at 1:05 PM Siek, Jeremy <jsiek at indiana.edu<mailto:jsiek at indiana.edu>> wrote:
I would like to define a function (Martello and Montanari’s unification algorithm)
whose termination measure is a lexicographic ordering of three numbers.
I get the impression that there is support for this kind of thing in the
standard library, in Induction.WellFounded.Lexicographic.
However, I’m at a loss trying to figure out how to use it.
Any examples or pointers to documentation or tutorials
would be much appreciated.

Thank you,
Jeremy





_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

__________________________________________
Jeremy G. Siek    <jsiek at indiana.edu<mailto:jsiek at indiana.edu>>
Professor
Luddy School of Informatics, Computing, and Engineering
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200229/d49ab369/attachment.html>