Programming Languages andCompilers (CS 421)Elsa L Gunter2112 SC, UIUChttp://www.cs.uiuc.edu/class/fa06/cs421/Based in part on slides by Mattox Beckman, as updatedby Vikram Adve and Gul AghaElsa L. GunterBackground 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 argumentsare base cases• Constructors applied to different number ofarguments (arity) considered different• Substitution of terms for variablesElsa L. GunterSimple ImplementationBackgroundtype 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. GunterUnification ProblemGiven a set of pairs of terms (“equations”){(s1, t1), (s2, t2), …, (sn, tn)}(the unification problem) does there exista substitution σ (the unification solution)of terms for variables such thatσ(si) = σ(ti),for all I = 1, …, n?Elsa L. GunterUses for Unification• Type Inference and type checking• Pattern matching as in OCAML– Can used a simplified version of algorithm• Logic Programming - Prolog• Simple parsingElsa L. GunterUnification Algorithm• Let S = {(s1, t1), (s2, t2), …, (sn, tn)} be aunification problem.• Case S = { }: Unif(S) = Identiy function(ie no substitution)• Case S = {(s, t)} ∪ S’): Four main stepsElsa L. GunterUnification Algorithm• Delete: if s = t (they are the same term)then Unif(S) = Unif(S’)• Decompose: if s = f(q1, … , qm) andt =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 nota variable, Unif(S) = Unif ({(x,s)} ∪ S’)Elsa L. GunterUnification Algorithm• Eliminate: if s = x is a variable,and x does not occur in t (theoccurs check), then–Let ϕ = x |→ t–Let ψ = Unif(ϕ(S’))–Unif(S) = {x |→ ψ(t)} o ψElsa L. GunterTricks for Efficient Unification• Don’t return substitution, rather doit incrementally• Make substitution be constant time– Requires implementation of terms touse mutable structures (or possiblylazy structures)– We haven’t discussed these yetElsa L. GunterExample• x,y,z variables, f,g constructors• S = {(f(x), f(g(y,z))), (g(y,f(y)),x)}Elsa L. GunterExample• 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. GunterExample• 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. GunterExample• x,y,z variables, f,g constructors• S -> {(f(x), f(g(y,z))), (x,g(y,f(y)))}Elsa L. GunterExample• 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. GunterExample• 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. GunterExample• 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. GunterExample• 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. GunterExample• 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. GunterExample• 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. GunterExample• 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. GunterExample• x,y,z variables, f,g constructors• Pick a pair: (y,y)• Eliminate• S -> {(f(y),z)}With {x |→ g(y,f(y))}Elsa L. GunterExample• 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. GunterExample• 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. GunterExample• 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. GunterExample• 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. GunterExample• 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. GunterExampleS = {(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. GunterExample 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...