CHANGELOG.md

@@ -1,5 +1,10 @@
 # Changelog
 
+## 0.9
+
+* Performance improvement: search tree pruning
+* Alpha equality check done lazily
+
 ## 0.8
 
 * Partial type inference for input formulas

src/main/java/pl/wojciechkarpiel/jhou/Api.java

@@ -165,6 +165,10 @@ public class Api {
         return Normalizer.betaEtaNormalForm(term);
     }
 
+    public static Term betaNormalEtaContracted(Term term) {
+        return etaContract(betaNormalize(term));
+    }
+
     public static Type typeOf(Term term) {
         return TypeCalculator.calculateType(term);
     }

src/main/java/pl/wojciechkarpiel/jhou/alpha/AlphaEqual.java

@@ -1,19 +1,17 @@
 package pl.wojciechkarpiel.jhou.alpha;
 
-import pl.wojciechkarpiel.jhou.ast.Abstraction;
-import pl.wojciechkarpiel.jhou.ast.Term;
-import pl.wojciechkarpiel.jhou.ast.Variable;
+import pl.wojciechkarpiel.jhou.ast.*;
 import pl.wojciechkarpiel.jhou.ast.type.Type;
+import pl.wojciechkarpiel.jhou.ast.util.Visitor;
 import pl.wojciechkarpiel.jhou.substitution.Substitution;
 import pl.wojciechkarpiel.jhou.substitution.SubstitutionPair;
 import pl.wojciechkarpiel.jhou.termHead.BetaEtaNormal;
 import pl.wojciechkarpiel.jhou.termHead.Head;
 import pl.wojciechkarpiel.jhou.util.ListUtil;
+import pl.wojciechkarpiel.jhou.util.MapUtil;
+import pl.wojciechkarpiel.jhou.util.Pair;
 
-import java.util.ArrayList;
-import java.util.HashSet;
-import java.util.List;
-import java.util.Optional;
+import java.util.*;
 import java.util.stream.Collectors;
 
 public class AlphaEqual {
@@ -22,14 +20,7 @@ public class AlphaEqual {
     }
 
     public static boolean isAlphaEqual(Abstraction a, Abstraction b) {
-        if (a.getVariable().equals(b.getVariable())) return a.getBody().equals(b.getBody());
-        if (!a.getVariable().getType().equals(b.getVariable().getType())) return false;
-        Variable v = Variable.freshVariable(a.getVariable().getType());
-        Substitution aSub = new Substitution(a.getVariable(), v);
-        Substitution bSub = new Substitution(b.getVariable(), v);
-        Term aVBody = aSub.substitute(a.getBody());
-        Term bVBody = bSub.substitute(b.getBody());
-        return aVBody.equals(bVBody);
+        return LazyAlphaEqual.isAlphaEqualLazy(a, b);
     }
 
 
@@ -88,21 +79,64 @@ public class AlphaEqual {
         return aLol.backToTerm().equals(bLol.backToTerm());
     }
 
-    public static class BenPair {
-        private final BetaEtaNormal left;
-        private final BetaEtaNormal right;
-
+    public static class BenPair extends Pair<BetaEtaNormal, BetaEtaNormal> {
         public BenPair(BetaEtaNormal left, BetaEtaNormal right) {
-            this.left = left;
-            this.right = right;
+            super(left, right);
+        }
+    }
+
+    private static class LazyAlphaEqual {
+
+        static boolean isAlphaEqualLazy(Term a, Term b) {
+            return new LazyAlphaEqual().alphaEqual(a, b);
         }
 
-        public BetaEtaNormal getLeft() {
-            return left;
+        private LazyAlphaEqual() {
+
         }
 
-        public BetaEtaNormal getRight() {
-            return right;
+        private final MapUtil<Variable, Variable> leftSub = new MapUtil<>(new HashMap<>());
+        private final MapUtil<Variable, Variable> rightSub = new MapUtil<>(new HashMap<>());
+
+        private boolean alphaEqual(Term left, Term right) {
+            return left.visit(new Visitor<Boolean>() {
+                @Override
+                public Boolean visitConstant(Constant constant) {
+                    return constant.equals(right);
+                }
+
+                @Override
+                public Boolean visitVariable(Variable variable) {
+                    Variable subL = leftSub.get(variable).orElse(variable);
+                    if (right instanceof Variable) {
+                        Variable subR = rightSub.get((Variable) right).orElse((Variable) right);
+                        return subL.equals(subR);
+                    } else return false;
+                }
+
+                @Override
+                public Boolean visitApplication(Application application) {
+                    if (right instanceof Application) {
+                        Application r = (Application) right;
+                        return alphaEqual(application.getFunction(), r.getFunction()) &&
+                                alphaEqual(application.getArgument(), r.getArgument());
+                    } else return false;
+                }
+
+                @Override
+                public Boolean visitAbstraction(Abstraction leftAbs) {
+                    if (right instanceof Abstraction) {
+                        Abstraction rightAbs = (Abstraction) right;
+                        if (rightAbs.getVariable().equals(leftAbs.getVariable()))
+                            return alphaEqual(leftAbs.getBody(), rightAbs.getBody());
+                        if (!rightAbs.getVariable().getType().equals(leftAbs.getVariable().getType())) return false;
+                        Variable newVar = Variable.freshVariable(rightAbs.getVariable().getType());
+                        return leftSub.withMapping(leftAbs.getVariable(), newVar,
+                                () -> rightSub.withMapping(rightAbs.getVariable(), newVar,
+                                        () -> alphaEqual(leftAbs.getBody(), rightAbs.getBody())));
+                    } else return false;
+                }
+            });
         }
     }
 }

src/main/java/pl/wojciechkarpiel/jhou/ast/util/FreeVariable.java

@@ -0,0 +1,60 @@
+package pl.wojciechkarpiel.jhou.ast.util;
+
+import pl.wojciechkarpiel.jhou.ast.*;
+import pl.wojciechkarpiel.jhou.util.MapUtil;
+
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Set;
+
+public class FreeVariable {
+    private FreeVariable() {
+    }
+
+    public static Set<Variable> getFreeVariables(Term term) {
+        FreeVariableCollector collector = new FreeVariableCollector();
+        collector.collect(term);
+        return collector.freeVariables;
+    }
+
+
+    private static class FreeVariableCollector {
+        final Set<Variable> freeVariables = new HashSet<>();
+        final MapUtil<Variable, Unit> boundVariables = new MapUtil<>(new HashMap<>());
+
+        Void collect(Term t) {
+            return t.visit(new Visitor<Void>() {
+                @Override
+                public Void visitConstant(Constant constant) {
+                    return null;
+                }
+
+                @Override
+                public Void visitVariable(Variable variable) {
+                    if (boundVariables.get(variable).isPresent()) return null;
+                    freeVariables.add(variable);
+                    return null;
+                }
+
+                @Override
+                public Void visitApplication(Application application) {
+                    collect(application.getFunction());
+                    collect(application.getArgument());
+                    return null;
+                }
+
+                @Override
+                public Void visitAbstraction(Abstraction abstraction) {
+                    boundVariables.withMapping(abstraction.getVariable(),
+                            Unit.INSTANCE,
+                            () -> collect(abstraction.getBody()));
+                    return null;
+                }
+            });
+        }
+    }
+
+    private enum Unit {
+        INSTANCE
+    }
+}

src/main/java/pl/wojciechkarpiel/jhou/substitution/Substitution.java

@@ -2,6 +2,7 @@ package pl.wojciechkarpiel.jhou.substitution;
 
 import pl.wojciechkarpiel.jhou.ast.*;
 import pl.wojciechkarpiel.jhou.ast.util.Visitor;
+import pl.wojciechkarpiel.jhou.normalizer.Normalizer;
 import pl.wojciechkarpiel.jhou.util.ListUtil;
 
 import java.util.ArrayList;
@@ -32,7 +33,8 @@ public class Substitution {
     public Term substitute(Term input) {
         Term result = input;
         for (SubstitutionPair substitutionPair : substitution) {
-            result = new Substituter(substitutionPair).substituteInt(result);
+            // might contain free variables if not beta-normalized. TODO: is it OK?
+            result = Normalizer.betaNormalize(new Substituter(substitutionPair).substituteInt(result));
         }
         return result;
     }
@@ -89,7 +91,6 @@ public class Substitution {
                 @Override
                 public Term visitAbstraction(Abstraction abstraction) {
                     Variable v = abstraction.getVariable();
-                    int i;
                     Optional<SubstitutionPair> oldPair = Optional.empty();
                     if (v.equals(Substituter.this.substitution.getVariable())) {
                         oldPair = Optional.of(Substituter.this.substitution);
@@ -99,9 +100,7 @@ public class Substitution {
                             abstraction.getVariable(),
                             substituteInt(abstraction.getBody())
                     );
-                    if (oldPair.isPresent()) {
-                        Substituter.this.substitution = oldPair.get();
-                    }
+                    oldPair.ifPresent(substitutionPair -> Substituter.this.substitution = substitutionPair);
                     return ret;
                 }
             });

src/test/java/pl/wojciechkarpiel/jhou/testUtil/TestUtil.java

@@ -1,8 +1,12 @@
 package pl.wojciechkarpiel.jhou.testUtil;
 
 import pl.wojciechkarpiel.jhou.ast.Term;
+import pl.wojciechkarpiel.jhou.ast.Variable;
+import pl.wojciechkarpiel.jhou.ast.util.FreeVariable;
 import pl.wojciechkarpiel.jhou.substitution.Substitution;
 
+import java.util.Set;
+
 import static org.junit.jupiter.api.Assertions.assertTrue;
 import static pl.wojciechkarpiel.jhou.Api.alphaBetaEtaEqual;
 
@@ -12,6 +16,20 @@ public class TestUtil {
         Term as = s.substitute(a);
         Term bs = s.substitute(b);
         assertTrue(alphaBetaEtaEqual(as, bs));
-        // TODO: check that there are no free variables!
+        Set<Variable> freeA = FreeVariable.getFreeVariables(as);
+        Set<Variable> freeB = FreeVariable.getFreeVariables(bs);
+
+        Set<Variable> origAfv = FreeVariable.getFreeVariables(a);
+        Set<Variable> origBfv = FreeVariable.getFreeVariables(b);
+        // todo not good, all FVs should be eliminated and exchanged for a constant, no leftovers
+        if (!freeA.isEmpty() || !freeB.isEmpty()) {
+            System.out.println("NO GOOD - LEFT FVs");
+        }
+        freeB.removeAll(origBfv);
+        freeA.removeAll(origBfv);
+        freeB.removeAll(origAfv);
+        freeA.removeAll(origAfv);
+        assertTrue(freeA.isEmpty());
+        assertTrue(freeB.isEmpty());
     }
 }