Unification and Matching

Intro

This notebook showcases Isabelle unification and matching from Elixir. We can send ordinary Isabelle theory text (unicode supported) such as:

unification pattern_unify "λx::i. (?F x :: i)" "λx::i. f (g x)"

and the checked theory returns the computed assignments as Isabelle output messages.

Behind the scenes, the command unification is defined in a small Isabelle support session:

• priv/isabelle/unification/ROOT declares the session IsabelleElixirUnification
• priv/isabelle/unification/Unification.thy contains the Isabelle/ML wrappers around Isabelle’s internal unification and matching functionality.

When using the published package, replace the dependency with {:isabelle_elixir, "~> 0.3"}.

Mix.install([
  {:isabelle_elixir, path: Path.expand("..", __DIR__)}
])

Start Isabelle

#System.put_env("ISABELLE_TOOL", "path/to/isabelle/executable") # optionally, if needed
IsabelleClient.Server.executable()

{:ok, server} =
  IsabelleClient.start_server(
    server_name: "livebook_unification_#{System.unique_integer([:positive])}"
  )

{:ok, client} = IsabelleClient.connect(server)

Start Session

The examples below import the session-qualified theory IsabelleElixirUnification.Unification. The relevant names are kept explicit:

• unification_root: directory containing the ROOT file
• unification_session: session name declared by that ROOT
• unification_import: theory imported by each generated check_text invocation

The final section also imports the TPTP/THF notation theory, so we load the bundled TPTP.thy into the same Isabelle session.

unification_root = Path.expand("../priv/isabelle/unification", __DIR__)
unification_session = "IsabelleElixirUnification"
unification_import = "IsabelleElixirUnification.Unification"
tptp_import = "TPTP"

%{
  root: unification_root,
  session: unification_session,
  import: unification_import,
  tptp_import: tptp_import,
  tptp_source: IsabelleClient.TPTP.source_path(),
  files: File.ls!(unification_root),
}

{:ok, client, start_task} =
  IsabelleClient.start_session(
    client,
    [
      session: unification_session,
      dirs: [unification_root],
      verbose: true
    ],
    120_000
  )

{:ok, tptp_task} = IsabelleClient.TPTP.load(client, 120_000)

%{
  session_id: IsabelleClient.active_session(client).id,
  start_messages: IsabelleClient.messages(start_task),
  tptp_messages: IsabelleClient.messages(tptp_task)
}

Checking Examples

Every example below sends a small Isabelle command string through IsabelleClient.TPTP.check/5, which wraps check_text/5 and filters out routine theory-progress messages. The remaining messages are produced by Isabelle itself.

IsabelleClient.TPTP.check(client, unification_import, "RawPatternUnify", ~S"""
typedecl i
consts f :: "i => i"
consts g :: "i ⇒ i" (* unicode supported *)

unification pattern_unify "λx::i. (?F x :: i)" "λx::i. f (g x)"
""")
|> IO.puts()

Type Unification and Matching

type_unify is type-unification: equation-solving over types. It invokes Isabelle’s Sign.typ_unify under the hood.

left_type = "('a list ⇒ j) ⇒ 'a list"
right_type = "(i list ⇒ 'b) ⇒ i list"

IsabelleClient.TPTP.check(client, unification_import, "TypeUnify", """
typedecl i
typedecl j

unification type_unify ‹#{left_type}› ‹#{right_type}›
""")
|> IO.puts()

type_match is one-way type matching. Variables in the first type are instantiated to make it match the second type. It invokes Isabelle’s Sign.typ_match under the hood.

type_pattern = "'b ⇒ 'a list"
type_object = "(i ⇒ j) ⇒ i list"

IsabelleClient.TPTP.check(client, unification_import, "TypeMatch", """
typedecl i
typedecl j

unification type_match ‹#{type_pattern}› ‹#{type_object}›
""")
|> IO.puts()

Higher-Order Pattern Unification and Matching

pattern_unify relies on Isabelle’s Pattern.unify, a deterministic higher-order pattern unifier.

left_term = "λx::i. ?F x"
right_term = "\\<lambda>x::i. f (g x)" # unicode input is optional

IsabelleClient.TPTP.check(client, unification_import, "PatternUnify", """
typedecl i
consts f :: "i ⇒ i"
consts g :: "i => i"

unification pattern_unify ‹#{left_term}› ‹#{right_term}›
""")
|> IO.puts()

The command reports fragment failures as messages instead of crashing. Here ?F is applied to the same bound variable twice, so it is not a higher-order pattern.

left_term = "λx::i. (?F x x :: i)"
right_term = "λx::i. f x"

IsabelleClient.TPTP.check(client, unification_import, "PatternFragmentFailure", """
typedecl i
consts f :: "i ⇒ i"

unification pattern_unify ‹#{left_term}› ‹#{right_term}›
""")
|> IO.puts()

pattern_match instantiates variables in the first term to match the second, by invoking Isabelle’s Pattern.match.

pattern = "h ?x (f ?y)"
object = "h a (f b)"

IsabelleClient.TPTP.check(client, unification_import, "PatternMatch", """
typedecl i
consts a :: i
consts b :: i
consts f :: "i ⇒ i"
consts h :: "i ⇒ i ⇒ i"

unification pattern_match ‹#{pattern}› ‹#{object}›
""")
|> IO.puts()

Use pattern_matches for a boolean answer.

pattern = "h ?x (f ?y)"
object = "h a (f b)"

IsabelleClient.TPTP.check(client, unification_import, "PatternMatches", """
typedecl i
consts a :: i
consts b :: i
consts f :: "i ⇒ i"
consts h :: "i ⇒ i ⇒ i"

unification pattern_matches ‹#{pattern}› ‹#{object}›
""")
|> IO.puts()

pattern_rewrite takes three arguments: target term, rewrite left-hand side, and rewrite right-hand side. It uses Isabelle’s Pattern.match_rew under the hood.

target = "h a (f b)"
lhs = "h ?x (f ?y)"
rhs = "h ?y (f ?x)"

IsabelleClient.TPTP.check(client, unification_import, "PatternRewrite", """
typedecl i
consts a :: i
consts b :: i
consts f :: "i ⇒ i"
consts h :: "i ⇒ i ⇒ i"

unification pattern_rewrite ‹#{target}› ‹#{lhs}› ‹#{rhs}›
""")
|> IO.puts()

Higher-Order (Pre-)Unification and Matching

unifiers relies on Isabelle’s Unify.unifiers as a general higher-order preunification procedure. Unlike Pattern.unify, it can search beyond the higher-order pattern fragment. In this example ?F is applied to the same bound variable twice, so it is not a pattern problem, but preunification still finds solutions.

left_term = "λx::i. (?F x x :: i)"
right_term = "λx::i. f x"

IsabelleClient.TPTP.check(client, unification_import, "PreunifiersBeyondPattern", """
typedecl i
consts f :: "i ⇒ i"

unification unifiers ‹#{left_term}› ‹#{right_term}›
""")
|> IO.puts()

Here is a case where Unify.unifiers deliberately preserves an unresolved flex-flex pair.

left_term = "λx::i. (?F x :: i)"
right_term = "λx::i. (?F (f x) :: i)"

IsabelleClient.TPTP.check(client, unification_import, "FlexFlexPreunifiers", """
typedecl i
consts f :: "i ⇒ i"

unification unifiers ‹#{left_term}› ‹#{right_term}›
""")
|> IO.puts()

smash_unifiers relies on Isabelle’s Unify.smash_unifiers, which additionally takes any remaining flex-flex pairs and applies a trivial substitution, so the result has no separate flex-flex output.

left_term = "λx::i. (?F x :: i)"
right_term = "λx::i. (?F (f x) :: i)"

IsabelleClient.TPTP.check(client, unification_import, "SmashedFlexFlexPreunifiers", """
typedecl i
consts f :: "i ⇒ i"

unification smash_unifiers ‹#{left_term}› ‹#{right_term}›
""")
|> IO.puts()

matchers builds upon Isabelle’s Unify.matchers, which does (one-way) higher-order matching. It returns all matchers.

pattern = "λx::i. (?F x :: i)"
object = "λx::i. f (g x)"

IsabelleClient.TPTP.check(client, unification_import, "Matchers", """
typedecl i
consts f :: "i ⇒ i"
consts g :: "i ⇒ i"

unification matchers ‹#{pattern}› ‹#{object}›
""")
|> IO.puts()

matcher builds upon Isabelle’s Unify.matcher, which is a convenience wrapper for matching two term lists that returns the first matcher, if one exists.

pattern = "λx::i. (?F x :: i)"
object = "λx::i. f (g x)"

IsabelleClient.TPTP.check(client, unification_import, "Matcher", """
typedecl i
consts f :: "i ⇒ i"
consts g :: "i ⇒ i"

unification matcher ‹#{pattern}› ‹#{object}›
""")
|> IO.puts()

TPTP/THF Syntax

This repeats the first higher-order preunification example, but the input term is written with the bundled THF notation from TPTP.

Here ^ [x : $i] : ... is THF-style lambda syntax and $i is the TPTP individual type. Application is left implicit as ?F x x and f x: in this support theory, explicit @ is the Isabelle constant thf_app, so using ?F @ x @ x would change the raw unification problem.

thf_import = "#{unification_import} #{tptp_import}"

IsabelleClient.TPTP.check(client, thf_import, "THFPreunifiersBeyondPattern", ~S"""
consts f :: "$i > $i"

unification unifiers "^ [x : $i] : (?F x x : $i)" "^ [x : $i] : f x"
""", from: true, show_thf_app: false)
|> IO.puts()

We can also have output in TPTP/THF-like syntax:

thf_import = "#{unification_import} #{tptp_import}"

IsabelleClient.TPTP.check(client, thf_import, "THFPreunifiersBeyondPattern", ~S"""
consts f :: "$i > $i"

unification unifiers "^ [x : $i] : (?F x x : $i)" "^ [x : $i] : f x"
""", from: true, to: true, show_thf_app: true)
|> IO.puts()

Stop the Session and Shutdown

{:ok, client, stop_task} = IsabelleClient.stop_session(client, 120_000)

%{
  remaining_sessions: client.sessions,
  messages: IsabelleClient.messages(stop_task)
}

IsabelleClient.shutdown_server(client)