Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: ML_Unification

view this post on Zulip Email Gateway (Oct 04 2023 at 16:01):

From: Dmitriy Traytel <traytel@di.ku.dk>
Hi all,

We have a new AFP entry in the Tools category, which constitutes a substantial extension to our favorite rule/erule/drule repertoire (and more):

Unification Utilities for Isabelle/ML
by Kevin Kappelmann

Abstract:

This article provides various unification utilities for Isabelle/ML, most prominently:

  1. First-order and higher-order pattern E-unification and E-matching. While unifiers in Isabelle/ML only consider the alpha-beta-eta-equational theory of the lambda-calculus, unifiers in this article may take an extra background theory, in the form of an equational prover, into account. For example, the unification problem "n+1 == ?m + Suc 0" may be solved by providing a prover for the background theory "!n. n+1 == n + Suc 0".
  2. Tactics, methods, and attributes with adjustable unifiers (e.g. resolution, fact, assumption, OF).
  3. A generalisation of unification hints. Unification hints are a flexible extension for unifiers. Among other things, they can be used for reflective tactics, to provide canonical unification instances, or to simply strengthen the background theory of a unifier in a controlled manner.
  4. Simplifier integration for e-unifiers.
  5. Practical combinations of unification algorithms, e.g. a combination of first-order and higher-order pattern unification.
  6. A hierarchical logger for Isabelle/ML, including per logger configurations with log levels, output channels, message filters.

While this entry works with every object logic, some extra setup for Isabelle/HOL and application examples are provided. All unifiers are tested with SpecCheck.

https://www.isa-afp.org/entries/ML_Unification.html

Good entry points are the example theories:

https://www.isa-afp.org/theories/ml_unification/#E_Unification_Examples
https://www.isa-afp.org/theories/ml_unification/#Unification_Hints_Reification_Examples

Enjoy!
Dmitriy

view this post on Zulip Email Gateway (Oct 05 2023 at 11:05):

From: Lawrence Paulson <lp15@cam.ac.uk>
This looks like fun! But I hope there is a paper explaining the ideas.

Larry

view this post on Zulip Email Gateway (Oct 10 2023 at 10:42):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
I am afraid, I do not have time to publish anything on this matter at
present. But much of it can be understood as a generalisation of
unification hints, introduced by Asperti et al. in "Hints in
Unification" (TPHOLs 2009):
https://link.springer.com/chapter/10.1007/978-3-642-03359-9_8

And of course, I am happy to help people that are interested in using
parts of this entry.

Kevin

Last updated: Jan 04 2025 at 20:18 UTC