<div dir="ltr"><br><div class="gmail_extra"><br>On Mon, Nov 18, 2013 at 11:35 AM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div class="im">On 2013-11-18 00:26, Kenichi Asai wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
I wonder if there is an agda implementation of Conor McBride's paper<br>
"First-order unification by structural recursion". Any information is<br>
welcome.<br>
</blockquote>
<br></div>
I believe that Andrea Vezzosi made use of this approach in his<br>
implementation of pattern unification:<br>
<br>
<a href="https://github.com/Saizan/miller" target="_blank">https://github.com/Saizan/<u></u>miller</a><div class="im"><br></div></blockquote><div><br></div><div>I indeed reuse many concepts there, but a few years before I had also implemented the original paper and the correctness proof[1] in Agda:</div>
<div><br></div><div> <a href="http://code.haskell.org/~Saizan/unification/">http://code.haskell.org/~Saizan/unification/</a></div><div><br></div><div>It was one of my first Agda programs and I've never put much effort into cleaning it up so the correctness proof is quite rough, though it should be readable with the paper on the side.</div>
<div><br></div><div>One complication is that it threads various extensionality proofs alongside "Property"'s so that we don't need to postulate functional extensionality.</div><div><br></div><div><br></div>
<div>[1] <a href="http://www.strictlypositive.org/foubsr-website/">http://www.strictlypositive.org/foubsr-website/</a></div><div><br></div><div><br></div><div>-- Andrea Vezzosi</div><div><br></div><div><br></div><div><br>
</div><div><br></div></div></div></div>