Programming Languages and Compilers (CS 421)Background for UnificationSimple Implementation BackgroundUnification ProblemUses for UnificationUnification AlgorithmSlide 7Slide 8Tricks for Efficient UnificationExampleSlide 11Slide 12Slide 13Slide 14Slide 15Slide 16Slide 17Slide 18Slide 19Slide 20Slide 21Slide 22Slide 23Slide 24Slide 25Slide 26Slide 27Example of FailureProgramming Languages and Compilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/sp07/cs421/Based in part on slides by Mattox Beckman, as updated by Vikram Adve and Gul AghaElsa L. Gunter Background for Unification•Terms made from constructors and variables (for the simple first order case)•Constructors may be applied to arguments (other terms) to make new terms•Variables and constructors with no arguments are base cases•Constructors applied to different number of arguments (arity) considered different•Substitution of terms for variablesElsa L. Gunter Simple Implementation Backgroundtype term = Variable of string | Const of (string * term list)let rec subst vn residue term = match term with Variable n -> if vn = n then residue else term | Const (c, tys) -> Const (c, List.map (subst vn residue) tys);;Elsa L. Gunter Unification ProblemGiven a set of pairs of terms (“equations”){(s1, t1), (s2, t2), …, (sn, tn)} (the unification problem) does there exist a substitution (the unification solution)of terms for variables such that(si) = (ti), for all I = 1, …, n?Elsa L. Gunter Uses for Unification•Type Inference and type checking•Pattern matching as in OCAML–Can use a simplified version of algorithm•Logic Programming - Prolog•Simple parsingElsa L. Gunter Unification Algorithm•Let S = {(s1, t1), (s2, t2), …, (sn, tn)} be a unification problem.•Case S = { }: Unif(S) = Identity function (ie no substitution)•Case S = {(s, t)} S’): Four main stepsElsa L. Gunter Unification Algorithm•Delete: if s = t (they are the same term) then Unif(S) = Unif(S’)•Decompose: if s = f(q1, … , qm) and t =f(r1, … , rm) (same f, same m!), then Unif(S) = Unif({(q1, r1), …, (qm, rm)} S’)•Orient: if t = x is a variable, and s is not a variable, Unif(S) = Unif ({(x,s)} S’)Elsa L. Gunter Unification Algorithm•Eliminate: if s = x is a variable, and x does not occur in t (the occurs check), then–Let = x | t–Let = Unif((S’))–Unif(S) = {x | (t)} o Elsa L. Gunter Tricks for Efficient Unification•Don’t return substitution, rather do it incrementally•Make substitution be constant time–Requires implementation of terms to use mutable structures (or possibly lazy structures)–We haven’t discussed these yetElsa L. Gunter Example•x,y,z variables, f,g constructors•S = {(f(x), f(g(y,z))), (g(y,f(y)),x)}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (g(y,f(y)),x)•S = {(f(x), f(g(y,z))), (g(y,f(y)),x)}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (g(y,f(y))),x)•Orient is first rule that applies•S = {(f(x), f(g(y,z))), (g(y,f(y)),x)}Elsa L. Gunter Example•x,y,z variables, f,g constructors•S -> {(f(x), f(g(y,z))), (x,g(y,f(y)))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (f(x), f(g(y,z)))•S -> {(f(x), f(g(y,z))), (x,g(y,f(y)))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (f(x), f(g(y,z)))•Decompose it (x, g(y,z))•S -> {(x, g(y,z)), (x,g(y,f(y)))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (x,g(y,f(y)))•S -> {(x, g(y,z)), (x,g(y,f(y)))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (x,g(y,f(y)))•Substitute:•S -> {(g(y,f(y)), g(y,z))}With {x | g(y,f(y))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (g(y,f(y)), g(y,z))•S -> {(g(y,f(y)), g(y,z))}With {x | g(y,f(y))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (g(y,f(y)), g(y,z))•Decompose: (y,y) and (f(y), z)•S -> {(y,y), (f(y),z)}With {x | g(y,f(y))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (y,y)•S -> {(y,y), (f(y),z)}With {x | g(y,f(y))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (y,y)•Delete•S -> {(f(y),z)}With {x | g(y,f(y))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (f(y),z)•S -> {(f(y),z)}With {x | g(y,f(y))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (f(y),z)•Orient•S -> {(z,f(y))}With {x | g(y,f(y))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (z,f(y))•S -> {(z,f(y))}With {x | g(y,f(y))}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (z,f(y))•Substitute•S -> { }With {x | {z | f(y)} (g(y,f(y)) } o {z | f(y)}Elsa L. Gunter Example•x,y,z variables, f,g constructors•Pick a pair: (z,f(y))•Substitute•S -> { }With {x | g(y,f(y))} o {(z | f(y))}Elsa L. Gunter ExampleS = {(f(x), f(g(y,z))), (g(y,f(y)),x)}Solved by {x | g(y,f(y))} o {(z | f(y))}f(g(y,f(y))) = f(g(y,f(y))) x zand g(y,f(y)) = g(y,f(y)) xElsa L. Gunter Example of Failure•S = {(f(x,g(y)), f(h(y),x))}•Decompose•S -> {(x,h(y)), (g(y),x)}•Orient•S -> {(x,h(y)), (x,g(y))}•Substitute•S -> {(h(y), g(y))} with {x | h(y)}•No rule to apply! Decompose
View Full Document
Unlocking...