2023-11-29-unification.tex (1903B)
1 \documentclass[../main.tex]{subfiles} 2 3 \begin{document} 4 5 \section{2023-11-29 Unification in LoA proofs} 6 7 At a particular point during interaction with the LoA assistant, 8 when we finally apply to a goal an assumption without 9 subassumptions, the system will perform the simplification 10 procedure on the goal tree. That procedure involves recursively 11 (depth-first) checking that each applied assumption indeed matches 12 the goal at that level. That is, \emph{after} substitution. And that 13 is the snag. Substitution, at this point, is what ends up demanding 14 of us that we bake variable bindings onto terms; of course, 15 otherwise, we'd have no way of knowing which variables we \emph{can} 16 and which variables we \emph{cannot} replace. 17 18 Let's look at this example: 19 20 \begin{lstlisting} 21 { 22 [tp] t param 23 [xp] x param 24 [xv] x var 25 xp 26 [tt] t term 27 tp 28 } [lambda-term] lam(x, t) term 29 \end{lstlisting} 30 31 If we want to prove that \lstinline{lam(x, x) term}, we'd proceed as 32 follows: 33 34 \begin{lstlisting} 35 { 36 [yp] y param 37 [yv] y var 38 yp 39 } ! id-term lam(y, y) term 40 lambda-term // push `lam(y, t) term` as candidate 41 // First subgoal: `t param` 42 var-term // Use `y term`; subgoal: `y var` 43 yv // Substitution: `t := y` 44 // Second subgoal: `y param` 45 var-term 46 yv // Substitution: `y := y` 47 // Third subgoal: `y var` 48 yv 49 // Fourth subgoal: `y term` 50 var-term 51 yv 52 \end{lstlisting} 53 54 The variable is a parameter on the assumption as well. Otherwise, 55 we'd have no way of using other variables that are not the one 56 mentioned verbatim on the subcontext of the assumption. That is, 57 things that are not parameters work almost like punctuation. 58 59 The above proof, compacted, would read: 60 61 \begin{lstlisting} 62 { @ yp (param y) @ yv (var y) yp } ! id-term (term (lam y y)) lambda-term var-term yv var-term yv yv var-term yv 63 \end{lstlisting} 64 65 \end{document}