∀x∀y (x=y iff ∀z , (z∈x iff z∈y )): Axiom of Extensionality in set theory

[TaviTruman]

I am staring to get a handle in using Guan but would like to run this by the community first. To test my understanding the foundations of Guan I thought I'd implement the "Axiom of Extensionality."

Here's me thinking out loud:

This first-order logic formula states that for every pair of sets x and y, x is equal to y if and only if for every element z, z is an element of x if and only if z is an element of y.

In other words, this formula asserts that two sets are equal if they have exactly the same elements. This is known as the Axiom of Extensionality in set theory, which is one of the fundamental principles of set theory. The symbols used are ∀ (for all), iff (if and only if), and ∈ (is an element of).

To express the Axiom of Extensionality in Guan, you'll need to define predicates to represent set membership (element of) and set equality. Here's an example of how you might implement the Axiom of Extensionality in Guan:

1. Define a new predicate type for set membership (element of):

public class ElementOfPredicateType : PredicateType
{
    // ... implementation details ...
}

2. Define a new predicate type for set equality:

public class SetEqualityPredicateType : PredicateType
{
    // ... implementation details ...
}

3. Implement the Axiom of Extensionality as a rule in Guan:

setEquality(X, Y) :- 
    forall(Z, implies(elementOf(Z, X), elementOf(Z, Y))),
    forall(Z, implies(elementOf(Z, Y), elementOf(Z, X))).

In this implementation, setEquality represents the equality of sets X and Y, and elementOf represents the membership of an element Z in a set X or Y. The forall keyword represents "for all," and the implies keyword represents "implies."

Please note that this is a high-level representation of how you might implement the Axiom of Extensionality in Guan. I know I need need to provide the specific implementation details for the ElementOfPredicateType and SetEqualityPredicateType classes, as well as register the predicates and rule in your Guan system.

Guam Implementation: (NOTE: this is NOT working code; not yet!)

I'll create a custom predicate for set membership (ElementOf) and set equality (SetEquality), then write a rule in Guan to represent the Axiom of Extensionality. Note that this example assumes you have already set up a Guan project and have knowledge of how to define custom predicates.

1. Define the ElementOfPredicateType class:

public class ElementOfPredicateType : PredicateType
{
    private static ElementOfPredicateType Instance;

    public static ElementOfPredicateType Singleton(string name)
    {
        return Instance ??= new ElementOfPredicateType(name);
    }

    private ElementOfPredicateType(string name)
        : base(name, true, 2, 2)
    {
    }

    public override PredicateResolver CreateResolver(CompoundTerm input, Constraint constraint, QueryContext context)
    {
        return new ElementOfResolver(input, constraint, context);
    }

    class ElementOfResolver : BooleanPredicateResolver
    {
        public ElementOfResolver(CompoundTerm input, Constraint constraint, QueryContext context)
            : base(input, constraint, context)
        {
        }

        protected override Task<bool> CheckAsync()
        {
            // Implement your set membership logic here.
            // For demonstration purposes, this example uses a simple list as a set representation.

            var element = Input.Arguments[0].Value.GetEffectiveTerm().GetObjectValue();
            var set = Input.Arguments[1].Value.GetEffectiveTerm().GetObjectValue() as List<object>;

            return Task.FromResult(set.Contains(element));
        }
    }
}

2. Define the SetEqualityPredicateType class:

public class SetEqualityPredicateType : PredicateType
{
    private static SetEqualityPredicateType Instance;

    public static SetEqualityPredicateType Singleton(string name)
    {
        return Instance ??= new SetEqualityPredicateType(name);
    }

    private SetEqualityPredicateType(string name)
        : base(name, true, 2, 2)
    {
    }

    public override PredicateResolver CreateResolver(CompoundTerm input, Constraint constraint, QueryContext context)
    {
        return new SetEqualityResolver(input, constraint, context);
    }

    class SetEqualityResolver : BooleanPredicateResolver
    {
        public SetEqualityResolver(CompoundTerm input, Constraint constraint, QueryContext context)
            : base(input, constraint, context)
        {
        }

        protected override Task<bool> CheckAsync()
        {
            var set1 = Input.Arguments[0].Value.GetEffectiveTerm().GetObjectValue() as List<object>;
            var set2 = Input.Arguments[1].Value.GetEffectiveTerm().GetObjectValue() as List<object>;

            return Task.FromResult(set1.Count == set2.Count && set1.All(x => set2.Contains(x)));
        }
    }
}

3. Register the custom predicates in your Guan system:

// Add custom predicates to the module
Module module = new Module("MyModule");
module. Add(ElementOfPredicateType.Singleton("elementOf"));
module. Add(SetEqualityPredicateType.Singleton("setEquality"));

4. Define the Axiom of Extensionality as a rule in Guan:

setEquality(X, Y) :-
    forall(Z, implies(elementOf(Z, X), elementOf(Z, Y))),
    forall(Z, implies(elementOf(Z, Y), elementOf(Z, X))).

Add this rule to Guan system as a string in your C# code:

string extensionalityRule = @"
setEquality(X, Y) :-
    forall(Z, implies(elementOf(Z, X), elementOf(Z, Y))),
    forall(Z, implies(elementOf(Z, Y), elementOf(Z, X))).
";
module.AddRule

Prototype Implementation: (NOT Ready for Use)

// ...
class Resolver : BooleanPredicateResolver
{
    public Resolver(CompoundTerm input, Constraint constraint, QueryContext context)
        : base(input, constraint, context)
    {
    }

    protected override Task<bool> CheckAsync()
    {
        int element = int.Parse(Input.Arguments[0].Value.GetEffectiveTerm().GetStringValue());
        IReadOnlyList<int> list = ParseList(Input.Arguments[1].Value.GetEffectiveTerm().GetStringValue());

        return Task.FromResult(list.Contains(element));
    }

    private IReadOnlyList<int> ParseList(string listString)
    {
        string[] items = listString.Split(new[] { ',' }, StringSplitOptions.RemoveEmptyEntries);
        List<int> list = new List<int>();

        foreach (string item in items)
        {
            list.Add(int.Parse(item.Trim()));
        }

        return list;
    }
}
// ...

// ...
class Resolver : BooleanPredicateResolver
{
    public Resolver(CompoundTerm input, Constraint constraint, QueryContext context)
        : base(input, constraint, context)
    {
    }

    protected override Task<bool> CheckAsync()
    {
        IReadOnlyList<int> list1 = ParseList(Input.Arguments[0].Value.GetEffectiveTerm().GetStringValue());
        IReadOnlyList<int> list2 = ParseList(Input.Arguments[1].Value.GetEffectiveTerm().GetStringValue());

        if (list1.Count != list2.Count)
        {
            return Task.FromResult(false);
        }

        HashSet<int> set1 = new HashSet<int>(list1);
        HashSet<int> set2 = new HashSet<int>(list2);

        return Task.FromResult(set1.SetEquals(set2));
    }

    private IReadOnlyList<int> ParseList(string listString)
    {
        string[] items = listString.Split(new[] { ',' }, StringSplitOptions.RemoveEmptyEntries);
        List<int> list = new List<int>();

        foreach (string item in items)
        {
            list.Add(int.Parse(item.Trim()));
        }

        return list;
    }
}

// ...

sing System;
using System.Collections.Generic;
using System.Threading.Tasks;
using Guan.Logic;

namespace GuanExamples
{
    public class GuanQueryDispatcher
    {
        private readonly Module module_;

        public GuanQueryDispatcher(Module module)
        {
            module_ = module;
        }

        public async Task RunQueryAsync(string queryExpression, int maxResults = 1)
        {
            // Required ModuleProvider instance. You created the module used in its construction in Program.cs.
            ModuleProvider moduleProvider = new ModuleProvider();
            moduleProvider.Add(module_);

            // Required QueryContext instance. You must supply moduleProvider (it implements IFunctorProvider).
            QueryContext queryContext = new QueryContext(moduleProvider);

            // The Query instance that will be used to execute the supplied query expression over the related rules.
            Query query = Query.Create(queryExpression, queryContext);

            // Execute the query. 
            // result will be () if there is no answer/result for supplied query (see the simple external predicate rules, for example).
            if (maxResults == 1)
            {
                // Gets one result.
                Term result = await query.GetNextAsync();
                Console.WriteLine($"answer: {result}"); // () if there is no answer.
            }
            else
            {
                // Gets multiple results, if possible, up to supplied maxResults value.
                List<Term> results = await query.GetResultsAsync(maxResults);
                Console.WriteLine($"answer: {string.Join(',', results)}"); // convert the List<Term> object into a comma-delimited string.
            }
        }
    }
}

using System;
using System.Collections.Generic;
using System.Threading.Tasks;
using Guan.Logic;
using GuanExamples.ExternalPredicates;

namespace GuanExamples
{
    class Program
    {
        static async Task Main(string[] args)
        {
            // Create a FunctorTable and register custom predicates
            var functorTable = new FunctorTable();
            functorTable.Add(ElementOfPredicateType.Singleton("elementOf"));
            functorTable.Add(SetEqualityPredicateType.Singleton("setEquality"));

            // Add the Axiom of Extensionality rule
            string extensionalityRule = @"
    setEquality(?X, ?Y) :-
        forall(?Z, implies(elementOf(?Z, ?X), elementOf(?Z, ?Y))),
        forall(?Z, implies(elementOf(?Z, ?Y), elementOf(?Z, ?X))).
";



            // Create a list of logic rules
            var logicRules = new List<string> { extensionalityRule };

            // Create a Module with the logic rules and FunctorTable
            Module module = Module.Parse("MyModule", logicRules, functorTable);

            // Create a GuanQueryDispatcher with the created module
            GuanQueryDispatcher queryDispatcher = new GuanQueryDispatcher(module);

            // Define sample sets
            List<object> setA = new List<object> { 1, 2, 3 };
            List<object> setB = new List<object> { 1, 2, 3 };
            List<object> setC = new List<object> { 1, 2, 4 };

            // Run a query to check if setA and setB are equal
            //await queryDispatcher.RunQueryAsync($"setEquality({Term.MakeConstant(setA)}, {Term.MakeConstant(setB)})");

            //// Run a query to check if setA and setC are equal
            //await queryDispatcher.RunQueryAsync($"setEquality({Term.MakeConstant(setA)}, {Term.MakeConstant(setC)})");

            // Run a query to check if setA and setB are equal
            await queryDispatcher.RunQueryAsync($"setEquality('1,2,3', '1,2,3')");

            // Run a query to check if setA and setC are equal
            await queryDispatcher.RunQueryAsync($"setEquality('1,2,3', '1,2,4')");



        }
    }
}

[TaviTruman]

Okay, I am now working to implement the concrete implementation, and have made the following changes:

1. Implement the CustomFunctionProvider class:

using Guan.Logic;

public class CustomFunctionProvider : IFunctionProvider
{
    public GuanFunc GetFunction(string name, int arity)
    {
        if (name == "elementOf" && arity == 2)
        {
            return ElementOfFunction.Singleton;
        }
        if (name == "all_elements_in" && arity == 2)
        {
            return AllElementsInFunction.Singleton;
        }
        if (name == "implies_element_of" && arity == 2)
        {
            return ImpliesElementOfFunction.Singleton;
        }

        return null;
    }
}

2. Implement the ElementOfFunction class:

using Guan.Logic;

internal class ElementOfFunction : BinaryFunc
{
    public static ElementOfFunction Singleton = new ElementOfFunction();

    protected ElementOfFunction() : base("elementOf")
    {
    }

    public override object BinaryInvoke(object arg1, object arg2)
    {
        // Assuming arg1 is the element and arg2 is the set represented as a list.
        return ((List<object>)arg2).Contains(arg1);
    }
}

3. Implement the AllElementsInFunction class:

using Guan.Logic;

internal class AllElementsInFunction : BinaryFunc
{
    public static AllElementsInFunction Singleton = new AllElementsInFunction();

    protected AllElementsInFunction() : base("all_elements_in")
    {
    }

    public override object BinaryInvoke(object arg1, object arg2)
    {
        // Assuming arg1 and arg2 are sets represented as lists.
        foreach (object item in (List<object>)arg1)
        {
            if (!((List<object>)arg2).Contains(item))
            {
                return false;
            }
        }

        return true;
    }
}
4. Implement the ImpliesElementOfFunction class:

using Guan.Logic;

internal class ImpliesElementOfFunction : BinaryFunc
{
    public static ImpliesElementOfFunction Singleton = new ImpliesElementOfFunction();

    protected ImpliesElementOfFunction() : base("implies_element_of")
    {
    }

    public override object BinaryInvoke(object arg1, object arg2)
    {
        // Assuming arg1 is the element and arg2 is the set represented as a list.
        return ((List<object>)arg2).Contains(arg1);
    }
}

When creating the Module, pass an instance of your custom IFunctionProvider to the Parse method:

IFunctionProvider customFunctionProvider = new CustomFunctionProvider();
Module module = Module.Parse("MyModule", ruleExpressions, customFunctionProvider, publicTypes);

[TaviTruman]

Okay - I want to explore the logic set design and implementation of Logic Programming in Guan. This is not 100% working code but we are getting closer.

1. First, create C# classes for the external predicates:

using Guan.Logic;

public class ShellPredicate : StandaloneFunc
{
    public static ShellPredicate Singleton = new ShellPredicate();

    private ShellPredicate() : base("Shell")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the Shell predicate logic here
    }
}

// Similarly, create classes for View, ViewModel, FiniteSet, UniqueId, UniqueName, Assigned predicates.

2. Register the external predicates in the FunctorTable:

var functorTable = new FunctorTable();
functorTable.Add(ShellPredicate.Singleton);
functorTable.Add(ViewPredicate.Singleton);
functorTable.Add(ViewModelPredicate.Singleton);
functorTable.Add(FiniteSetPredicate.Singleton);
functorTable.Add(UniqueIdPredicate.Singleton);
functorTable.Add(UniqueNamePredicate.Singleton);
functorTable.Add(AssignedPredicate.Singleton);
functorTable.Add(PairPredicate.Singleton);
functorTable.Add(ContainsPredicate.Singleton);
functorTable.Add(ElementOfPredicate.Singleton);

3. We need to write the code the External Predicates

using Guan.Logic;

public class ViewPredicate : StandaloneFunc
{
    public static ViewPredicate Singleton = new ViewPredicate();

    private ViewPredicate() : base("View")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the View predicate logic here
    }
}

public class ViewModelPredicate : StandaloneFunc
{
    public static ViewModelPredicate Singleton = new ViewModelPredicate();

    private ViewModelPredicate() : base("ViewModel")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the ViewModel predicate logic here
    }
}

public class FiniteSetPredicate : StandaloneFunc
{
    public static FiniteSetPredicate Singleton = new FiniteSetPredicate();

    private FiniteSetPredicate() : base("FiniteSet")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the FiniteSet predicate logic here
    }
}

public class UniqueIdPredicate : StandaloneFunc
{
    public static UniqueIdPredicate Singleton = new UniqueIdPredicate();

    private UniqueIdPredicate() : base("UniqueId")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the UniqueId predicate logic here
    }
}

public class UniqueNamePredicate : StandaloneFunc
{
    public static UniqueNamePredicate Singleton = new UniqueNamePredicate();

    private UniqueNamePredicate() : base("UniqueName")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the UniqueName predicate logic here
    }
}

public class AssignedPredicate : StandaloneFunc
{
    public static AssignedPredicate Singleton = new AssignedPredicate();

    private AssignedPredicate() : base("Assigned")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the Assigned predicate logic here
    }
}

public class PairPredicate : StandaloneFunc
{
    public static PairPredicate Singleton = new PairPredicate();

    private PairPredicate() : base("Pair")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the Pair predicate logic here
    }
}

public class ContainsPredicate : StandaloneFunc
{
    public static ContainsPredicate Singleton = new ContainsPredicate();

    private ContainsPredicate() : base("Contains")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the Contains predicate logic here
    }
}

public class ElementOfPredicate : StandaloneFunc
{
    public static ElementOfPredicate Singleton = new ElementOfPredicate();

    private ElementOfPredicate() : base("ElementOf")
    {
    }

    public override object Invoke(object[] args)
    {
        // Implement the ElementOf predicate logic here
    }
}

4. Define the Guan rules:

var logicRules = new List<string>
{
    "existsShell :- Shell(?x)",
    "existsFiniteSet :- FiniteSet(?S), forall(?x, implies(Shell(?x), elementOf(?x, ?S)))",
    "shellContainsViewViewModelPair :- forall(?x, implies(Shell(?x), exists(?y, ?z, View(?y), ViewModel(?z), pair(?y, ?z), contains(?x, pair(?y, ?z)))))",
    "uniqueIds :- forall(?x, ?y, implies(and(or(Shell(?x), View(?x), ViewModel(?x)), or(Shell(?y), View(?y), ViewModel(?y)), not(equal(?x, ?y))), not(equal(UniqueId(?x), UniqueId(?y)))))",
    "uniqueNames :- forall(?x, implies(or(Shell(?x), View(?x), ViewModel(?x)), existsUnique(?n, UniqueName(?n), Assigned(?x, ?n))))"
};

5. Parse the module and create a GuanQueryDispatcher:

Module module = Module.Parse("guan_example", logicRules, functorTable);
var queryDispatcher = new GuanQueryDispatcher(module);

6. Execute queries based on the rules:

await queryDispatcher.RunQueryAsync("existsShell");
await queryDispatcher.RunQueryAsync("existsFiniteSet");
await queryDispatcher.RunQueryAsync("shellContainsViewViewModelPair");
await queryDispatcher.RunQueryAsync("uniqueIds");
await queryDispatcher.RunQueryAsync("uniqueNames");