Stream: Isabelle/ML

Topic: wrong unifier: meta variables of function types


view this post on Zulip Kevin Kappelmann (Aug 26 2021 at 13:53):

I am confused about the behaviour of Unify.unifiers in the following situation:

ML
  val t =
    Var (("v", 0), TFree ("'a", []) --> TFree ("'b", [])) $
      Var (("w", 0), TFree ("'a", []))
  val s =
    Var (("x", 0), TFree ("'a", []) --> TFree ("'b", [])) $
      Var (("y", 0), TFree ("'a", []))
  (*returns empty environment and no unification error (unifying (t, s))*)
  val env =
    Unify.unifiers ((Context.the_generic_context ()), Envir.init, [(t,s)]) |> Seq.hd |> fst

  (*returns correct unifier for (t, s')*)
  val s' = (Var (("x", 0), TFree ("'b", [])))
  val env' =
    Unify.unifiers ((Context.the_generic_context ()), Envir.init, [(t, s')]) |> Seq.hd |> fst

how come that in the first case, an empty environment is returned?

view this post on Zulip Kevin Kappelmann (Sep 01 2021 at 13:11):

Nevermind - I misinterpreted the way unifiersworks. I thought it returns a sequence of environments including instantiations for flex-flex pairs, but indeed it returns a sequence of environments including instantiations only for non-flex-flex cases and all remaining flex-flex instances in a separate list.


Last updated: Jul 15 2022 at 23:21 UTC