Practice with Unification

Your browser lacks required capabilities. Please upgrade it or switch to another to continue.

Loading…

! Log in (We will not ask for a password.) <<nobr>> <<set $code0 to 0>> <</nobr>> EPantherID: <<textboxplus "$name" "guest" autofocus>> <<set $code0 to jtb.icHash($name+setup.semester)>> <<set $badchars to jtb.badLogin($name)>> <<if setup.logins.includes($name)>><<goto "LoggedIn">><<else>> <<replace "#login-error">><<if $badchars isnot "">> An EPantherID cannot include characters such as $badchars.<<else>> The EPantherID $name is not registered with the class.<</if>> [[Proceed without credit->LoggedIn]]<</replace>><</if>> <</textboxplus>>@uwm.edu <span id="login-error"></span>

<<set $current to "Introduction">> <<goto "Definitions">>

! Unification This web page is designed to help people learn unification, including higher-order unification, such as used in Twelf and SASyLF. !! Definitions !!! Concrete Structure A //concrete structure// is a tree where every node is labeled with a //constructor// and may have 0 or more subtrees. An arbitrary node may be displayed using the notation > //label// [...] where the "..." is a possibly empty, comma-separated sequence of subtrees. If the sequence is empty, the square brackets //may// be omitted. Examples # {{{zero[]}}} //or// {{{zero}}} # {{{plus[zero,succ[zero],succ[zero]]}}} # {{{plus-succ[plus[zero,succ[zero],succ[zero]], plus[succ[zero],succ[zero],succ[succ[zero]]]]}}} As these examples show, this low-level syntax can be difficult to read, although indentation can help. We will often display structures using a context-free grammar in which parentheses are added to avoid ambiguity. Suppose that we have the following representations: > <table> <tr><th>node syntax</th><th>natural syntax</th></tr> <tr><td>{{{zero[]}}}</td><td>0</td></tr> <tr><td>{{{succ[n]}}}</td><td>S {{{n}}}</td></tr> <tr><td>{{{plus[n1,n2,n3]}}}</td><td>{{{n1}}} + {{{n2}}} = {{{n3}}}</td></tr> <tr><td>{{{plus-succ[p1,p2]}}} </td> <td> p1 -- p2 </td></tr></table> Then we can represent our last example as > 0 + (S 0) = (S 0) > -------------------- > (S 0) + (S 0) = (S S 0) !!! Pattern Variables and Patterns //Pattern variables// are drawn from a set of identifiers distinct from those used for labels. In Twelf, pattern variables are Capitalized, in SASyLF, they are declared as //nonterminals// with optional numeric and prime versions. Uses of pattern variables can occur in structures, which are now no longer //concrete// structures but //pattern// structures (//patterns// for short). //Higher-order// pattern variables are those that take parameters in the same way as constructors. Higher-order pattern variables are used in SASyLF (and Twelf), but are beyond what this introduction covers. Here are a few examples of patterns: # {{{succ[succ[n]]}}} # {{{plus[zero,n,n]}}} # {{{plus-succ[plus[n1,n2,n3],plus[succ[n1], n2, succ[n3]]]}}} And we can use the same way to display patterns as we use to display concrete structures. For example the last pattern can be shown as > n1 + n2 = n3 > ------------- > S n1 + n2 = S n3 !!! Substitution A //substitution// is a map from pattern variables to patterns (not always concrete). A well-formed substitution has no overlap between its domain and the set of pattern variables used in its range. For instance, well-formed substitution cannot map {{{n}}} to {{{succ[n]}}}. It cannot even map {{{n}}} to {{{succ[n1]}}} if it also has a mapping for {{{n1}}} as well. A substitution {{{s}}} is applied to a pattern {{{p}}} (written "{{{s p}}}") by replacing any instance of the pattern variable in the pattern by what the substitution maps it to. Other pattern variables are unaffected. /*If pattern variables have arguments, the arguments are substituted in the same way. */ For example if we apply the substitution { n → {{{succ[n']}}}, n1 → {{{n2}}} } to the previous examples, we get (respectively) # {{{succ[succ[succ[n']]]}}} # {{{plus[zero,succ[n'],succ[n']]}}} # {{{plus-succ[plus[n2,n2,n3],plus[succ[n2],n2,succ[n3]]]}}} Two substitutions {{{s1}}} and {{{s2}}} can be composed by creating a compound substitution that includes all the mapping of the first substitution in which the result has the second substitution applied to it and then all mappings of the second substitution that do not map a variable already mapped by the first. For example, if > s1 = { n1 → {{{succ[n2]}}} }, s2 = { n2 → {{{zero}}}, n1 → {{{zero}}} } Then > s1 &compfn; s2 = { n1 → {{{succ[zero]}}}, n2 → {{{zero}}} } !!! Unification Unification in Computer Science is a pattern matching task in which a substitution {{{s}}} is found to //unify// two patterns {{{p1}}} and {{{p2}}}, that is {{{s p1}}} is exactly the same as {{{s p2}}}. Usually we want a //most general// unifier //u//: any other unifier //s// can be represented as //u// &compfn; //t// (for some substitution //t//). For example, suppose we have the two patterns: {{{0 + n = n}}} and {{{n1 + n2 = n3}}}, there any many unifiers including: # { n1 → {{{0}}}, n2 → n3 } # { n1 → {{{0}}}, n2 → {{{S 0}}}, n3 → {{{S 0}}} } The second unifier can be expressed by composing the first with { n3 → {{{S 0}}} }. [[Continue|$current]]

[[Definitions]] In this interactive web page, you will get practice with substitutions and unification. You will type in answers in text boxes and then press the 'Submit' button. If your answer is incorrect, you will asked to try again. Often there will be a 'Hint' button which will give a hint to the answer. For your practice, we have <<= setup.substs.length>> substitution exercises and <<= setup.unify.length>> unification exercises. <<set $i to 0>><<set $result to "">>[[Start|Subst Exercise]]

!! Substitution Exercise <<=$i+1>> of <<=setup.substs.length>><<if $i gte setup.substs.length>><<goto "Subst Exercise Done">><</if>><<set $current to "Subst Exercise">><<set _subst to setup.substs[$i]>> For the following input and the given substitution, please give the result of applying the substitution to the input. Fill in the text box and then press the [Submit] button. Do not use parentheses {{{(...)}}} or spaces in your answer. Input: <tt><<= _subst.input>></tt> <table style="border-spacing:0px"><tr><td>Substitution:</td><th>variable</th><th>pattern</th></tr>\ <<for _k, _v range _subst.subst>><tr><td></td><td style="text-align:center">_k</td><td><tt>_v</tt></td></tr>\ <</for>></table> Result: <<textbox "$result" "" autofocus>> <<button "Submit">> <<set _in to _subst.input>> <<set _sub to _subst.subst>> <<set _answer to setup.applySubst(_sub,_in)>> <<set $key0 to setup.icHash(_answer)>> <<replace "#comment" t8n>><<if _answer is $result>>Correct! <<link "Continue">><<set $i += 1>> <<goto "Subst Exercise">><</link>> <<elseif setup.similar($result,_answer)>>Very close! <<elseif $result.match(/[( )]/) isnot null>>Don't include parentheses or spaces. <<else>>Not correct<</if>><</replace>> <</button>> <<if def _subst.hint>><<button "Hint">> <<replace "#comment" t8n>><<= _subst.hint>><</replace>> <</button>><</if>> <span id="comment"></span> [[Review Definitions|Definitions]]

Congratulations! You have completed all the substitution exercises. Next it's on to the unification exercises.<<set $i to 0>> [[Continue|Unify Exercise]]

!! Unification Exercise <<=$i+1>> of <<=setup.unify.length>><<if $i gte setup.unify.length>><<goto "Unify Exercise Done">><</if>><<set $current to "Unify Exercise">><<set _unify to setup.unify[$i]>> <span id="instructions"><<if $i is 0>><<include "Unify Instructions">><<else>><<linkreplace "⊕ Instructions">><<include "Unify Instructions">><</linkreplace>><</if>></span> Input1: <tt><<= _unify.input1>></tt> Input2: <tt><<= _unify.input2>></tt> <table><tr><td>Substitution:</td><th>variable</th><th/><th>pattern</th></tr>\ <<for _k range _unify.vars>><<set _boxname to "$"+"value"+_k>><tr><td></td><td style="text-align:center">_k</td><td>→</td><td><tt><<textbox _boxname "">></tt></td></tr>\ <</for>></table> Result: <<textbox "$result" "">> <<button "Submit">> <<include "Unify Helper">> <<set _res1 to setup.applySubst(_sub,_unify.input1)>> <<set _res2 to setup.applySubst(_sub,_unify.input2)>> <<if def _unify.subst>> <<set _res to setup.applySubst(_unify.subst,_unify.input1)>> <<set _comp to setup.compareSubst(_sub,_unify.subst,_unify.vars)>> <<set $key to setup.icHash(_res1)>> <</if>> <<replace "#comment" t8n>> \<<if _problem isnot "">><<= _problem>> <<linkreplace "More...">>See for instance <<= _problemvar>><</linkreplace>>. \<<elseif _res1 isnot $result>>The result of applying the substitution to the first input is not correct<<if setup.similar(_res1,$result)>>, but it's very close<</if>>. \<<elseif _res1 isnot _res2>>The substitution does not unify the two inputs. <<linkreplace "More...">>The result of applying the substitution to the second input is <<= _res2>>.<</linkreplace>> \<<elseif setup.lengthSubst(_sub) gt setup.lengthSubst(_unify.subst) >>The substitution does unnecessary substitution. <<linkreplace "More...">>Perhaps your substitution of <<=_comp>> is incorrect.<</linkreplace>> \<<elseif _res1.length gt _res.length>>The substitution given is not the //most general// unifier of the two inputs. <<linkreplace "More...">>Perhaps your substitution of <<=_comp>> is incorrect.<</linkreplace>> \<<elseif _comp isnot null>>The substitution isn't what I expect. Perhaps it doesn't preferentially substitute earlier variables? <<linkreplace "More...">>The substitution of <<=_comp>> does not match what I expect.<</linkreplace>> \<<else>>Correct!<br><<link "Continue">><<set $i += 1>> <<goto "Unify Exercise">><</link>> \<</if>><</replace>> <</button>> \ <<button "Impossible">> <<include "Unify Helper">> <<set _res1 to setup.applySubst(_sub,_unify.input1)>> <<replace "#comment" t8n>> \<<if _problem isnot "">><<= _problem>> <<linkreplace "More...">>See for instance <<= _problemvar>><</linkreplace>>. \<<elseif _res1 isnot $result>>The result of applying the substitution to the first input is not correct<<if setup.similar(_res1,$result)>>, but it's very close<</if>>. \<<elseif def _unify.subst>>Actually unification is possible. Check out the hint if you haven't already. \<<else>>Correct! The inputs //cannot// be unified.<br><<link "Continue">><<set $i += 1>> <<goto "Unify Exercise">><</link>> \<</if>><</replace>> <</button>> \ <<if def _unify.hint>><<button "Hint">> <<replace "#comment" t8n>><<= _unify.hint>><</replace>> <</button>><</if>> <span id="comment"></span> <<link "Back">> <<if $i is 0>> <<goto "Subst Exercise Done">> <<else>> <<set $i -= 1>> <<goto "Unify Exercise">> <</if>> <</link>> [[Review Definitions|Definitions]]

<<link "⊖">><<replace "#instructions">><<linkreplace "⊕ Instructions">><<include "Unify Instructions">><</linkreplace>><</replace>> <</link>>\ For the following two inputs, determine a most general substitution that unifies them. Specify that substitution by filling in the boxes, and then fill in the unified output that results from applying the substitution to the first input. It should also be the result of applying the same substitution to the second input. Then hit "Submit". But sometimes unification is impossible. In that case, still fill in the result of applying the substitution to the first input, but hit the "Impossible" button, instead. In either case, the substitution should be well-formed--leave the "pattern" blank if the variable should //not// be mapped. Recall that a well-formed substitution cannot use a variable in the pattern mapped for a variable if the first variable is mapped in the substitution. Sometimes, there are multiple "most general unifications." In that case, prefer the substitution that maps the earliest variable possible.

<<set _sub to {}>> <<set _problem to "">> <<set _problemvar to "">> <<for _k range _unify.vars>> <<set _v to State.variables["value"+_k]>> <<if _v.match(/[() ]/) isnot null>> <<set _problem to "Don't use blanks or parentheses.">> <<set _problemvar to _k>> <<elseif _v isnot "">> <<set _sub[_k] to State.variables["value"+_k]>> <</if>> <</for>> <<if _problem is "">> <<set _problemvar to setup.checkSubst(_sub)>> <<if _problemvar isnot null>> <<set _problem to "The substitution is not well-formed.">> <<elseif $result.match(/[() ]/) isnot null>> <<set _problem to "Don't use blanks or parentheses.">> <<set _problemvar to "Result">> <</if>> <</if>>

Congratulations! You have completed all the unification exercises. The proof of your completion is the following number, please write it down. <<=jtb.comb3($key0,$key,$code0)>> [[Start Over|Introduction]] [[Review Definitions|Definitions]]