<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
Dear Matthew,
<div class=""><br class="">
</div>
<div class="">Thank you so much!</div>
<div class=""><br class="">
</div>
<div class="">I now have a terminating implementation of</div>
<div class=""><span style="font-family: TimesNewRomanPSMT;" class="">Martello and Montanari’s classic unification algorithm.</span></div>
<div class=""><span style="font-family: TimesNewRomanPSMT;" class=""><br class="">
</span></div>
<div class=""><span style="font-family: TimesNewRomanPSMT;" class="">This is for a graduate course in programming languages at Indiana University</span></div>
<div class=""><font face="TimesNewRomanPSMT" class="">based on PLFA:</font></div>
<div class=""><font face="TimesNewRomanPSMT" class=""><a href="https://jsiek.github.io/B522-PL-Foundations/" class="">https://jsiek.github.io/B522-PL-Foundations/</a></font></div>
<div class=""><font face="TimesNewRomanPSMT" class=""><br class="">
</font></div>
<div class=""><font face="TimesNewRomanPSMT" class="">Cheers,</font></div>
<div class=""><font face="TimesNewRomanPSMT" class="">Jeremy</font></div>
<div class=""><font face="TimesNewRomanPSMT" class=""><br class="">
</font>
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Feb 29, 2020, at 4:07 AM, Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" class="">matthewdaggitt@gmail.com</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" class="">Hi Jeremy,
<div class=""> 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. <a href="https://stackoverflow.com/questions/19642921/assisting-agdas-termination-checker" class="">
here</a>.</div>
<div class=""><br class="">
</div>
<div class="">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 `<a href="https://github.com/agda/agda-stdlib/pull/1094" class="">lexicographic-product</a>`
branch. The proof will however be available in the upcoming v1.3 release.</div>
<div class=""><br class="">
</div>
<div class="">In the meantime I think the easiest way for you to solve this problem is to copy the updated <a href="https://raw.githubusercontent.com/agda/agda-stdlib/03209af78061fdf734521359985c9de836e063b8/src/Data/Product/Relation/Binary/Lex/Strict.agda" class="">file</a>
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.</div>
<div class=""><br class="">
</div>
<div class="">```agda</div>
<div class="">module Test where<br class="">
<br class="">
open import Data.Nat<br class="">
open import Data.Nat.Induction using (Acc; acc; <-wellFounded)<br class="">
open import Data.Nat.Properties using (≤-refl)<br class="">
open import Data.Sum using (inj₁; inj₂)<br class="">
open import Data.Product<br class="">
open import Data.Product.Relation.Binary.Lex.Strict<br class="">
open import Induction.WellFounded using (WellFounded)<br class="">
open import Relation.Binary<br class="">
open import Relation.Binary.PropositionalEquality using (_≡_; refl)<br class="">
<br class="">
-- Define the order over the 3-tuples using two applications of `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict`:</div>
<div class=""><br class="">
_<₃_ : Rel (ℕ × ℕ × ℕ) _<br class="">
_<₃_ = ×-Lex _≡_ _<_ (×-Lex _≡_ _<_ _<_)<br class="">
<br class="">
-- Use the new `×-wellFounded` combinator to prove that the lexicographic ordering is well-founded:</div>
<div class=""><br class="">
<₃-wellFounded : WellFounded _<₃_<br class="">
<₃-wellFounded = ×-wellFounded <-wellFounded (×-wellFounded <-wellFounded <-wellFounded)<br class="">
<br class="">
-- The naive implementation of this function fails to pass the termination checker<br class="">
{-<br class="">
-- BAD: termination checking failure<br class="">
f : ℕ × ℕ × ℕ → ℕ<br class="">
f (x , zero , z) = z<br class="">
f (x , suc y , z) = f (x , y , suc z)<br class="">
-}<br class="">
<br class="">
-- Define a new function that takes in a decreasing Acc proof as well, and hence is acceptable to the termination checker</div>
<div class=""><br class="">
f-acc : ∀ (x : ℕ) → Acc _<₃_ x → ℕ<br class="">
f-acc (x , zero , z) rec = z<br class="">
f-acc (x , suc y , z) (acc rec) = f-acc (x , y , suc z)<br class="">
(rec _ (inj₂ (refl , inj₁ ≤-refl))) -- proof that the tuple is decreasing lexicographically<br class="">
<br class="">
-- Use <₃-wellFounded to provide the Acc proof
<div class=""></div>
f : ℕ × ℕ × ℕ → ℕ<br class="">
f xyz = f-acc xyz (<₃-wellFounded xyz)<br class="">
</div>
<div class="">```</div>
<div class=""><br class="">
</div>
<div class="">Best,</div>
<div class="">Matthew</div>
</div>
<br class="">
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sat, Feb 29, 2020 at 4:08 PM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com" class="">matthewdaggitt@gmail.com</a>> wrote:<br class="">
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div dir="ltr" class="">Hi Jeremy,
<div class=""> 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! </div>
<div class=""><br class="">
</div>
<div class="">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.</div>
<div class="">Best,</div>
<div class="">Matthew</div>
<div class=""><br class="">
</div>
</div>
<br class="">
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sat, Feb 29, 2020 at 1:05 PM Siek, Jeremy <<a href="mailto:jsiek@indiana.edu" target="_blank" class="">jsiek@indiana.edu</a>> wrote:<br class="">
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div class="">I would like to define a function (Martello and Montanari’s unification algorithm)
<div class="">whose termination measure is a lexicographic ordering of three numbers.</div>
<div class="">I get the impression that there is support for this kind of thing in the</div>
<div class="">standard library, in Induction.WellFounded.Lexicographic.</div>
<div class="">However, I’m at a loss trying to figure out how to use it.</div>
<div class="">Any examples or pointers to documentation or tutorials</div>
<div class="">would be much appreciated.</div>
<div class=""><br class="">
</div>
<div class="">Thank you,</div>
<div class="">Jeremy</div>
<div class=""><br class="">
<div class="">
<div class="">
<div dir="auto" style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; text-decoration: none;" class="">
<div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;" class="">
<div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;" class="">
<div style="letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;" class="">
<div class=""><br class="">
</div>
</div>
</div>
</div>
</div>
<br class="">
<br class="">
</div>
<br class="">
</div>
</div>
</div>
_______________________________________________<br class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
</blockquote>
</div>
</blockquote>
</div>
</div>
</blockquote>
</div>
<br class="">
<div class="">
<div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div style="color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
<div class=""><span style="font-family: Menlo; font-size: medium; orphans: 2; widows: 2;" class="">__________________________________________</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Jeremy G. Siek <<a href="mailto:jsiek@indiana.edu" class="">jsiek@indiana.edu</a>></span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Professor</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Luddy School of Informatics, Computing, and Engineering</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class="">Indiana University Bloomington</span><br style="font-family: Menlo; orphans: 2; widows: 2;" class="">
<span style="font-family: Menlo; orphans: 2; widows: 2;" class=""><a href="http://homes.soic.indiana.edu/jsiek/" class="">http://homes.soic.indiana.edu/jsiek/</a></span><br class="">
</div>
<div class=""><span style="font-family: Menlo; orphans: 2; widows: 2;" class=""><br class="">
</span></div>
</div>
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
</div>
<br class="Apple-interchange-newline">
<br class="Apple-interchange-newline">
</div>
<br class="">
</div>
</body>
</html>