From b2f76bdd8414db953c14bb799dfaabc79d882418 Mon Sep 17 00:00:00 2001 From: Cassie Jones Date: Thu, 20 Feb 2020 20:22:59 +0100 Subject: [PATCH] Clarify the first sentence of the unification post --- posts/2020/syntactic-unification.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/2020/syntactic-unification.md b/posts/2020/syntactic-unification.md index 4fc9e14..7e3466d 100644 --- a/posts/2020/syntactic-unification.md +++ b/posts/2020/syntactic-unification.md @@ -9,7 +9,7 @@ summary: "Last year I tried implementing syntactic unification and got completel --- Syntactic unification is the process of trying to find an assignment of variables that makes two terms the same. -For example, `(X, Y) = (1, 2)` would give the substitution `{X: 1, Y: 2}`, but `(X, X) = (1, 2)` would fail to unify. +For example, attempting to unify the terms in the equation `(X, Y) = (1, 2)` would give the substitution `{X: 1, Y: 2}`, but if we tried to uninfy `(X, X) = (1, 2)` it would fail since one variable can't be equal to two different values. Unification is used to implement two things I'm very interested in: type systems, and logic programming languages. Earlier last year I tried implementing unification in order to make a toy Prolog, and I got completely stuck on the algorithms. -- 2.43.2