Skip to content

Instantly share code, notes, and snippets.

@m1dnight
Created June 15, 2016 11:30
Show Gist options
  • Save m1dnight/ae0c25accec0d54a7974757fafa4a9aa to your computer and use it in GitHub Desktop.
Save m1dnight/ae0c25accec0d54a7974757fafa4a9aa to your computer and use it in GitHub Desktop.
module UnificationLearning
// Unification algorithm
//
// Portions Copyright (C) 2012 by Tomas Petricek
// Copyright (C) 2012 by Eric Taucher
// License: Creative Commons BY-SA Version 3.0
//
// This code is derived from a StackOverflow answer by Tomas Petricek
// See: http://stackoverflow.com/a/9525471/1243762
//
// In short, this is a reference and learning version, not a production version.
//
// This is an implementation of the Robinson algorithm without using unify to update unify's structures.
// If you look carefully at most functional implementations of the Robinson unification algorithm you will see that they
// are recursive and that they also use the unify function to update the internal structures.
// It would be like using regular expressions inside of a regular expression engine.
// You have to know regular expressions in order to understand the regular expression engine.
// Works if you already know it, but for a first introduction, it is quite confusing.
//
// Since this is my first use of a functional language, and I needed to understand the unification algorithm in detail,
// I did this implementation, which is actually the last version in a series of axiomatic progressions;
// thus the names with 900.
//
// Because this was done as an axiomatic progression, it has full traceability for finding bugs.
// Because of the way the sub functions are implemented it allows one to understand what is going on
// without having to compare the internal data structures before and after a function call.
// Because of the way the sub functions are implemented, I can give meaningful names to each step,
// instead of trying to factor out the steps in my head and keep track of the level of recursion.
type Expr900 =
| Value900 of int
| Variable900 of string
| Structure900 of string * Expr900 list
type Substution900 =
| ValueSubstution900 of string * int
| VariableSubtution900 of string * string
| StructureSubtution900 of string * string * Expr900 list
// Define occurs check function
let rec occursIn var xs =
match xs with
| (Value900 y)::xs1 -> occursIn var xs1
| (Variable900 y)::xs1 when var = y -> true
| (Variable900 y)::xs1 when var <> y -> occursIn var xs1
| (Structure900(s,l))::xs1 ->
let result = occursIn var l
match result with
| true -> true
| false -> occursIn var xs1
| [] -> false
| _ -> failwith "How did we get here?"
let unify900 xs ys =
// Define unify function
let rec unify xs ys mgu =
// Define replace function
let replace sub x y mgu =
// Define replacePattern function
let rec replacePattern sub xs =
// Define replacePatternUtil function
let rec replacePatternUtil sub xs acc =
match sub with
| ValueSubstution900(var,value) ->
match xs with
| (Structure900(f,l))::xs1 -> replacePatternUtil sub xs1 ((Structure900(f,(replacePattern sub l)))::acc)
| (Variable900 x)::xs1 when x = var -> replacePatternUtil sub xs1 ((Value900 value)::acc)
| (Variable900 x)::xs1 -> replacePatternUtil sub xs1 ((Variable900 x)::acc)
| (Value900 x)::xs1 -> replacePatternUtil sub xs1 ((Value900 x)::acc)
| [] -> (List.rev acc)
| _ -> failwith "How did we get here?"
| VariableSubtution900(var1,var2) ->
match xs with
| (Structure900(f,l))::xs1 -> replacePatternUtil sub xs1 ((Structure900(f,(replacePattern sub l)))::acc)
| (Variable900 x)::xs1 when x = var1 -> replacePatternUtil sub xs1 ((Variable900 var2)::acc)
| (Variable900 x)::xs1 -> replacePatternUtil sub xs1 ((Variable900 x)::acc)
| (Value900 x)::xs1 -> replacePatternUtil sub xs1 ((Value900 x)::acc)
| [] -> (List.rev acc)
| _ -> failwith "How did we get here?"
| StructureSubtution900(var,f,l) ->
match xs with
| (Structure900(f,l))::xs1 -> replacePatternUtil sub xs1 ((Structure900(f,(replacePattern sub l)))::acc)
| (Variable900 x)::xs1 when x = var -> replacePatternUtil sub xs1 ((Structure900(f,l))::acc)
| (Variable900 x)::xs1 -> replacePatternUtil sub xs1 ((Variable900 x)::acc)
| (Value900 x)::xs1 -> replacePatternUtil sub xs1 ((Value900 x)::acc)
| [] -> (List.rev acc)
| _ -> failwith "How did we get here?"
// Call replacePatternUtil function
// printfn "Before replacePatternUtil: substution: %A pattern: %A" sub xs
let result = replacePatternUtil sub xs []
// printfn "After replacePatternUtil: substution: %A pattern: %A \n" sub result
// return result
result
// Define updateMgu function
let rec updateMgu sub mgu =
// Define replaceMguUtil function
let rec replaceMguUtil sub mgu acc =
match mgu with
| ((ValueSubstution900(mguVar,mguTerm))::xs1)
-> replaceMguUtil sub xs1 ((ValueSubstution900(mguVar,mguTerm))::acc)
| ((VariableSubtution900(mguVar1,mguVar2))::xs1)
-> replaceMguUtil sub xs1 ((VariableSubtution900(mguVar1,mguVar2))::acc)
| ((StructureSubtution900(mguVar,f,l))::xs1)
-> replaceMguUtil sub xs1 ((StructureSubtution900(mguVar,f,(replacePattern sub l)))::acc)
| []
-> (List.rev acc)
// Call replaceMguUtil function saving result
let replacedMgu = replaceMguUtil sub mgu []
// append the new substution to the updated mgu
// While this is not a best practice,
// its obvious that sub is being appended to the mgu
replacedMgu@[sub]
// Call unify function
unify (replacePattern sub x) (replacePattern sub y) (updateMgu sub mgu)
// Define unifyStructure function
// Note: The mgu from the structure, i.e. structureMgu, is passed as the mgu for the remaining unfication.
// If not, then how would the final mgu be able to include the mgu from the substructure?
let unifyStructure s1 s2 xs ys mgu =
let (structureResult,structureMgu) = unify s1 s2 mgu
match structureResult with
| true -> unify xs ys structureMgu
| false -> (false, [])
// Define unifyUtil function
let unifyUtil xs ys mgu =
match xs with
| (Value900 x)::xs1 ->
match ys with
| (Value900 y)::ys1 when x = y -> unify xs1 ys1 mgu
| (Value900 y)::ys1 when x <> y -> (false, [])
| (Variable900 y)::ys1 -> replace (ValueSubstution900(y,x)) xs1 ys1 mgu
| (Structure900 _)::ys1 -> (false, [])
| [] -> (false, [])
| _ -> failwith "How did we get here?"
| (Variable900 x)::xs1 ->
match ys with
| (Value900 y)::ys1 -> replace (ValueSubstution900(x,y)) xs1 ys1 mgu
| (Variable900 y)::ys1 when x = y -> unify xs1 ys1 mgu
| (Variable900 y)::ys1 when x <> y -> replace (VariableSubtution900(x,y)) xs1 ys1 mgu
| (Structure900(s1,l1))::ys1 when occursIn x l1 -> (false, [])
| (Structure900(s1,l1))::ys1 -> replace (StructureSubtution900(x,s1,l1)) xs1 ys1 mgu
| [] -> (false, [])
| _ -> failwith "How did we get here?"
| (Structure900(s1,l1))::xs1 ->
match ys with
| (Value900 y)::ys1 -> (false, [])
| (Variable900 y)::ys1 when occursIn y l1 -> (false, [])
| (Variable900 y)::ys1 -> replace (StructureSubtution900(y,s1,l1)) xs1 ys1 mgu
| (Structure900(s2,l2))::ys1 when (s1 = s2) && (l1.Length = l2.Length) -> unifyStructure l1 l2 xs1 ys1 mgu
| (Structure900(s2,l2))::ys1 when (s1 <> s2) || (l1.Length <> l2.Length) -> (false, [])
| [] -> (false, [])
| _ -> failwith "How did we get here?"
| [] -> (true, mgu)
// Call unifyUtil function
unifyUtil xs ys mgu
// Call unify function
unify xs ys []
//#######################################
// Test x | f(x)
let unify901 =
let expr001 = [Variable900("x")]
let expr002 = [Structure900("f",[Variable900("x")])]
printfn "Unify test: unify901 - \n\t expr 1: %A \n\t expr 2: %A" expr001 expr002
let result = unify900 expr001 expr002
let res, mgu = result
printfn "\t result: %b mgu: %A \n" res mgu
// OK, that works
//----------------------------------------
// Test a,f(b,b) | 1,f(1,b)
let unify902 =
let expr001 = [Variable900("a");Structure900("f",[Variable900("b");Variable900("b")])]
let expr002 = [Value900(1);Structure900("f",[Value900(1);Variable900("b")])]
printfn "Unify test: unify902 - \n\t expr 1: %A \n\t expr 2: %A" expr001 expr002
let result = unify900 expr001 expr002
let res, mgu = result
printfn "\t result: %b mgu: %A \n" res mgu
// OK, that works
//----------------------------------------
// This is called from C# as
//
// private static void UnificationTest()
// {
// UnificationLearning.tests();
//
// Console.WriteLine("Press Enter to continue. ");
// Console.ReadLine();
// }
let tests() =
unify901
unify902
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment