Added some extension methods for Terms to the SentenceManipulation.Va…

…riableManipulation namespace.

Specifically, added IsInstanceOf, IsGeneralisationOf and Ordinalise. This logic was implemented as part of term indexing - but it would potentially be of use to consumers, so there's no sense in not making it public.

src/SCFirstOrderLogic.Alternatives/TermIndexing/PathTree_GradualVarBinding.cs

@@ -1,10 +1,8 @@
 // Copyright (c) 2021-2024 Simon Condon.
 // You may use this file in accordance with the terms of the MIT license.
 using SCFirstOrderLogic.SentenceManipulation;
-using System;
-using System.Collections.Generic;
+using SCFirstOrderLogic.SentenceManipulation.VariableManipulation;
 using System.Diagnostics.CodeAnalysis;
-using System.Linq;
 
 namespace SCFirstOrderLogic.TermIndexing;
 

src/SCFirstOrderLogic.Alternatives/TermIndexing/PathTree_WOVarBinding.cs

@@ -1,6 +1,7 @@
 // Copyright (c) 2021-2024 Simon Condon.
 // You may use this file in accordance with the terms of the MIT license.
 using SCFirstOrderLogic.SentenceManipulation;
+using SCFirstOrderLogic.SentenceManipulation.VariableManipulation;
 using System.Diagnostics.CodeAnalysis;
 
 namespace SCFirstOrderLogic.TermIndexing;

src/SCFirstOrderLogic.Tests/SentenceManipulation/VariableManipulation/TermExtensionsTests.cs

@@ -0,0 +1,52 @@
+using FluentAssertions;
+using FlUnit;
+using static SCFirstOrderLogic.SentenceCreation.OperableSentenceFactory;
+
+namespace SCFirstOrderLogic.SentenceManipulation.VariableManipulation;
+
+public static class TermExtensionsTests
+{
+    public static Test OrdinaliseBehaviourTests => TestThat
+        .GivenEachOf<OrdinaliseTestCase>(() =>
+        [
+            new(Input: F(), Expected: F()),
+            new(Input: F(X), Expected: F(Var(0))),
+            new(Input: F(G(X, Y), G(X, Z)), Expected: F(G(Var(0), Var(1)), G(Var(0), Var(2)))),
+        ])
+        .When(tc => tc.Input.Ordinalise())
+        .ThenReturns()
+        .And((tc, rv) => rv.Should().Be(tc.Expected));
+
+    public static Test IsInstanceOfBehaviourTests => TestThat
+        .GivenEachOf<BinaryTestCase>(() =>
+        [
+            new(X: F(), Y: F(), Expected: true),
+            new(X: F(A), Y: F(X), Expected: true),
+            new(X: F(G(Y, A)), Y: F(X), Expected: true),
+            new(X: F(X), Y: F(A), Expected: false),
+            new(X: F(X, A), Y: F(A, X), Expected: false),
+        ])
+        .When(tc => tc.X.IsInstanceOf(tc.Y))
+        .ThenReturns((tc, rv) => rv.Should().Be(tc.Expected));
+
+    public static Test IsGeneralisationOfBehaviourTests => TestThat
+        .GivenEachOf<BinaryTestCase>(() =>
+        [
+            new(X: F(), Y: F(), Expected: true),
+            new(X: F(X), Y: F(A), Expected: true),
+            new(X: F(X), Y: F(G(Y, A)), Expected: true),
+            new(X: F(A), Y: F(X), Expected: false),
+            new(X: F(X, A), Y: F(A, X), Expected: false),
+        ])
+        .When(tc => tc.X.IsGeneralisationOf(tc.Y))
+        .ThenReturns((tc, rv) => rv.Should().Be(tc.Expected));
+
+    private static OperableFunction A => new Function(nameof(A));
+    private static OperableFunction B => new Function(nameof(B));
+    private static OperableFunction F(params Term[] arguments) => new Function(nameof(F), arguments);
+    private static OperableFunction G(params Term[] arguments) => new Function(nameof(G), arguments);
+
+    private record OrdinaliseTestCase(Term Input, Term Expected);
+
+    private record BinaryTestCase(Term X, Term Y, bool Expected);
+}

src/SCFirstOrderLogic/SentenceManipulation/VariableManipulation/TermExtensions.cs

@@ -0,0 +1,144 @@
+using System.Collections.Generic;
+using System.Diagnostics.CodeAnalysis;
+
+namespace SCFirstOrderLogic.SentenceManipulation.VariableManipulation;
+
+/// <summary>
+/// Useful variable manipulation and inspection methods for <see cref="Term"/> instances.
+/// </summary>
+public static class TermExtensions
+{
+    /// <summary>
+    /// <para>
+    /// Ordinalises a term; replacing all variable identifiers with the (zero-based) ordinal of where they
+    /// first appear in a depth-first traversal of the term.
+    /// </para>
+    /// <para>
+    /// This is useful because it makes the original identifiers irrelevant but preserves distinctness, so that 
+    /// e.g. F(X, X) is transformed to a term that is identical to the transformation of F(Y, Y), but different
+    /// to the transformation of F(X, Y). Making the original identifier irrelevant is useful when e.g. indexing.
+    /// </para>
+    /// </summary>
+    /// <param name="term">The term to ordinalise.</param>
+    /// <returns>The ordinalised term.</returns>
+    public static Term Ordinalise(this Term term)
+    {
+        return term.Accept(new VariableOrdinalisation());
+    }
+
+    /// <summary>
+    /// Checks whether "this" term is an instance of another.
+    /// </summary>
+    /// <param name="term">The potential instance.</param>
+    /// <param name="generalisation">The generalisation.</param>
+    /// <returns>A value indicating whether "this" term is an instance of the generalisation.</returns>
+    public static bool IsInstanceOf(this Term term, Term generalisation)
+    {
+        return InstanceUnifier.TryCreate(generalisation, term, out _);
+    }
+
+    /// <summary>
+    /// Checks whether "this" term is a generalisation of another.
+    /// </summary>
+    /// <param name="term">The potential generalisation.</param>
+    /// <param name="instance">The instance.</param>
+    /// <returns>A value indicating whether "this" term is an generalisation of the instance.</returns>
+    public static bool IsGeneralisationOf(this Term term, Term instance)
+    {
+        return InstanceUnifier.TryCreate(term, instance, out _);
+    }
+
+    /// <summary>
+    /// <para>
+    /// Sentence transformation that converts all variable identifiers to the integer value of their order in a depth-first traversal of the sentence.
+    /// </para>
+    /// <para>
+    /// Useful in e.g. indexing, where we want to make the original identifier irrelevant when comparing sentences/clauses/terms.
+    /// </para>
+    /// </summary>
+    private class VariableOrdinalisation : RecursiveSentenceTransformation
+    {
+        private readonly Dictionary<object, VariableDeclaration> variableIdMap = new();
+
+        /// <inheritdoc/>
+        public override VariableDeclaration ApplyTo(VariableDeclaration variable)
+        {
+            if (!variableIdMap.TryGetValue(variable.Identifier, out var declaration))
+            {
+                declaration = variableIdMap[variable.Identifier] = new VariableDeclaration(variableIdMap.Count);
+            }
+
+            return declaration;
+        }
+    }
+
+    /// <summary>
+    /// Unification logic that is "one-way" - only allows variables present in one of the arguments (the "generalisation") to be substituted.
+    /// </summary>
+    private static class InstanceUnifier
+    {
+        public static bool TryCreate(Term generalisation, Term instance, [MaybeNullWhen(false)] out VariableSubstitution unifier)
+        {
+            var unifierAttempt = new MutableVariableSubstitution();
+
+            if (TryUpdateInPlace(generalisation, instance, unifierAttempt))
+            {
+                unifier = unifierAttempt.CopyAsReadOnly();
+                return true;
+            }
+
+            unifier = null;
+            return false;
+        }
+
+        private static bool TryUpdateInPlace(Term generalisation, Term instance, MutableVariableSubstitution unifier)
+        {
+            return (generalisation, instance) switch
+            {
+                (VariableReference variable, _) => TryUpdateInPlace(variable, instance, unifier),
+                (Function functionX, Function functionY) => TryUpdateInPlace(functionX, functionY, unifier),
+                // Below, the only potential for equality is if they're both constants. Perhaps worth testing this
+                // versus that explicitly and a default that just returns false. Similar from a performance
+                // perspective.
+                _ => generalisation.Equals(instance),
+            };
+        }
+
+        private static bool TryUpdateInPlace(VariableReference variable, Term instanceTerm, MutableVariableSubstitution unifier)
+        {
+            if (variable.Equals(instanceTerm))
+            {
+                return true;
+            }
+            else if (unifier.Bindings.TryGetValue(variable, out var variableValue))
+            {
+                // The variable is already mapped to something - we need to make sure that the
+                // mapping is consistent with the "other" value.
+                return TryUpdateInPlace(variableValue, instanceTerm, unifier);
+            }
+            else
+            {
+                unifier.AddBinding(variable, instanceTerm);
+                return true;
+            }
+        }
+
+        private static bool TryUpdateInPlace(Function x, Function y, MutableVariableSubstitution unifier)
+        {
+            if (!x.Identifier.Equals(y.Identifier) || x.Arguments.Count != y.Arguments.Count)
+            {
+                return false;
+            }
+
+            for (int i = 0; i < x.Arguments.Count; i++)
+            {
+                if (!TryUpdateInPlace(x.Arguments[i], y.Arguments[i], unifier))
+                {
+                    return false;
+                }
+            }
+
+            return true;
+        }
+    }
+}

src/SCFirstOrderLogic/TermIndexing/(Internals)/PathTreeHelpers.cs

@@ -1,7 +1,6 @@
 // Copyright (c) 2021-2024 Simon Condon.
 // You may use this file in accordance with the terms of the MIT license.
 using SCFirstOrderLogic.InternalUtilities;
-using SCFirstOrderLogic.SentenceManipulation;
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.CodeAnalysis;
@@ -31,24 +30,6 @@ public static IPathTreeArgumentNodeKey ToNodeKey(this Term term)
         };
     }
 
-    /// <summary>
-    /// <para>
-    /// Ordinalises a term; replacing all variable identifiers with the ordinal of where they
-    /// first appear in a depth-first traversal of the term (zero for the first, one for the second, and so on).
-    /// </para>
-    /// <para>
-    /// This is useful because it makes the original identifiers irrelevant but preserves distinctness, so that 
-    /// e.g. F(X, X) is transformed to a term that is identical to the transformation of F(Y, Y), but different
-    /// to the transformation of F(X, Y).
-    /// </para>
-    /// </summary>
-    /// <param name="term">The term to ordinalise.</param>
-    /// <returns>The ordinalised term.</returns>
-    public static Term Ordinalise(this Term term)
-    {
-        return term.Accept(new VariableOrdinalisation());
-    }
-
     /// <summary>
     /// Gets the set of values that appear in all of the inner enumerables.
     /// </summary>
@@ -151,97 +132,4 @@ public static bool TryGetCommonValue<T>(this IEnumerable<IEnumerable<T>> values,
             await enumerator.DisposeAsync();
         }
     }
-
-    /// <summary>
-    /// Checks whether "this" term is an instance of another.
-    /// </summary>
-    /// <param name="term">The potential instance.</param>
-    /// <param name="generalisation">The generalisation.</param>
-    /// <returns>A value indicating whether "this" term is an instance of the generalisation.</returns>
-    public static bool IsInstanceOf(this Term term, Term generalisation)
-    {
-        return InstanceUnifier.TryCreate(generalisation, term, out _);
-    }
-
-    private class VariableOrdinalisation : RecursiveSentenceTransformation
-    {
-        private readonly Dictionary<object, VariableDeclaration> variableIdMap = new();
-
-        public override VariableDeclaration ApplyTo(VariableDeclaration variable)
-        {
-            if (!variableIdMap.TryGetValue(variable.Identifier, out var declaration))
-            {
-                declaration = variableIdMap[variable.Identifier] = new VariableDeclaration(variableIdMap.Count);
-            }
-
-            return declaration;
-        }
-    }
-
-    private static class InstanceUnifier
-    {
-        public static bool TryCreate(Term generalisation, Term instance, [MaybeNullWhen(false)] out VariableSubstitution unifier)
-        {
-            var unifierAttempt = new MutableVariableSubstitution();
-
-            if (TryUpdateInPlace(generalisation, instance, unifierAttempt))
-            {
-                unifier = unifierAttempt.CopyAsReadOnly();
-                return true;
-            }
-
-            unifier = null;
-            return false;
-        }
-
-        private static bool TryUpdateInPlace(Term generalisation, Term instance, MutableVariableSubstitution unifier)
-        {
-            return (generalisation, instance) switch
-            {
-                (VariableReference variable, _) => TryUpdateInPlace(variable, instance, unifier),
-                (Function functionX, Function functionY) => TryUpdateInPlace(functionX, functionY, unifier),
-                // Below, the only potential for equality is if they're both constants. Perhaps worth testing this
-                // versus that explicitly and a default that just returns false. Similar from a performance
-                // perspective.
-                _ => generalisation.Equals(instance),
-            };
-        }
-
-        private static bool TryUpdateInPlace(VariableReference variable, Term instanceTerm, MutableVariableSubstitution unifier)
-        {
-            if (variable.Equals(instanceTerm))
-            {
-                return true;
-            }
-            else if (unifier.Bindings.TryGetValue(variable, out var variableValue))
-            {
-                // The variable is already mapped to something - we need to make sure that the
-                // mapping is consistent with the "other" value.
-                return TryUpdateInPlace(variableValue, instanceTerm, unifier);
-            }
-            else
-            {
-                unifier.AddBinding(variable, instanceTerm);
-                return true;
-            }
-        }
-
-        private static bool TryUpdateInPlace(Function x, Function y, MutableVariableSubstitution unifier)
-        {
-            if (!x.Identifier.Equals(y.Identifier) || x.Arguments.Count != y.Arguments.Count)
-            {
-                return false;
-            }
-
-            for (int i = 0; i < x.Arguments.Count; i++)
-            {
-                if (!TryUpdateInPlace(x.Arguments[i], y.Arguments[i], unifier))
-                {
-                    return false;
-                }
-            }
-
-            return true;
-        }
-    }
 }

src/SCFirstOrderLogic/TermIndexing/AsyncPathTree{TValue}.cs

@@ -2,6 +2,7 @@
 // You may use this file in accordance with the terms of the MIT license.
 using SCFirstOrderLogic.InternalUtilities;
 using SCFirstOrderLogic.SentenceManipulation;
+using SCFirstOrderLogic.SentenceManipulation.VariableManipulation;
 using System;
 using System.Collections.Generic;
 using System.Linq;

src/SCFirstOrderLogic/TermIndexing/PathTree{TValue}.cs

@@ -1,6 +1,7 @@
 // Copyright (c) 2021-2024 Simon Condon.
 // You may use this file in accordance with the terms of the MIT license.
 using SCFirstOrderLogic.SentenceManipulation;
+using SCFirstOrderLogic.SentenceManipulation.VariableManipulation;
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.CodeAnalysis;