diff --git a/docs/update_demonstrations_docs.py b/docs/update_demonstrations_docs.py index c3c0cf4..883b33d 100755 --- a/docs/update_demonstrations_docs.py +++ b/docs/update_demonstrations_docs.py @@ -100,10 +100,6 @@ def generate_demonstrations_docs(): ): rst_content += f"**Arity**: {concept.example_structure.input_arity}\n\n" - # Add symbolic definition if available - if hasattr(concept, "symbolic_definition"): - rst_content += "This concept is formally defined in the FRAME expression language.\n\n" - # Show computational implementation availability if hasattr(concept, "computational_implementation"): rst_content += "The concept has a computational implementation that can execute on concrete values.\n\n" diff --git a/frame/environments/math_env.py b/frame/environments/math_env.py index 2fe2a7a..8227ecc 100644 --- a/frame/environments/math_env.py +++ b/frame/environments/math_env.py @@ -374,7 +374,6 @@ def step(self, action: Union[int, ValidAction], is_simulation: bool = False) -> theorem = Theorem( name=new_entity.name, description=new_entity.description, - symbolic_definition=new_entity._symbolic, proof=cached_proof, example_structure=new_entity.examples.example_structure, lean4_translation=new_entity._lean4, @@ -422,7 +421,6 @@ def step(self, action: Union[int, ValidAction], is_simulation: bool = False) -> theorem = Theorem( name=new_entity.name, description=new_entity.description, - symbolic_definition=new_entity._symbolic, proof=proof, example_structure=new_entity.examples.example_structure, lean4_translation=new_entity._lean4, diff --git a/frame/knowledge_base/demonstrations.py b/frame/knowledge_base/demonstrations.py index a414cbb..2446589 100644 --- a/frame/knowledge_base/demonstrations.py +++ b/frame/knowledge_base/demonstrations.py @@ -32,7 +32,6 @@ addition = Concept( name="add", description="Addition of natural numbers defined by repeated succession", - symbolic_definition=lambda a, b: Fold(b, a, Lambda("x", Succ(Var("x")))), computational_implementation=lambda a, b: a + b, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -47,9 +46,6 @@ multiplication = Concept( name="multiply", description="Multiplication of natural numbers defined by repeated addition", - symbolic_definition=lambda a, b: Fold( - b, Zero(), Lambda("x", addition(Var("x"), a)) - ), computational_implementation=lambda a, b: a * b, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -65,9 +61,6 @@ divides = Concept( name="divides", description="a divides b if there exists n such that b = a*n", - symbolic_definition=lambda a, b: Exists( - "n", NatDomain(), Equals(b, multiplication(a, Var("n"))) - ), computational_implementation=lambda a, b: a == 0 and b == 0 # Special case: 0 divides 0 or a != 0 @@ -85,9 +78,6 @@ less_than = Concept( name="less_than", description="a < b if there exists m such that b = a + succ(m)", - symbolic_definition=lambda a, b: Exists( - "m", NatDomain(), Equals(b, addition(a, Succ(Var("m")))) - ), computational_implementation=lambda a, b: a < b, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -103,19 +93,6 @@ proper_divisors = Concept( name="proper_divisors", description="The set of proper divisors of n (positive divisors less than n)", - symbolic_definition=lambda n: Set( - domain=NatDomain(), - predicate=Lambda( - "d", - And( - And( - ConceptApplication(divides, Var("d"), n), - ConceptApplication(less_than, Zero(), Var("d")), - ), - ConceptApplication(less_than, Var("d"), n), - ), - ), - ), computational_implementation=lambda n: {i for i in range(1, n) if n % i == 0}, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -128,18 +105,6 @@ is_prime = Concept( name="is_prime", description="A number greater than 1 whose number of divisors is exactly 2", - symbolic_definition=lambda n: And( - ConceptApplication(less_than, Nat(1), n), - Equals( - SetCardinality( - Set( - domain=NatDomain(), - predicate=Lambda("k", ConceptApplication(divides, Var("k"), n)), - ) - ), - Nat(2), - ), - ), computational_implementation=lambda n: n > 1 and all(n % i != 0 for i in range(2, int(n**0.5) + 1)), example_structure=ExampleStructure( @@ -158,9 +123,6 @@ is_perfect = Concept( name="is_perfect", description="A number that equals the sum of its proper divisors", - symbolic_definition=lambda n: Equals( - n, SetSum(ConceptApplication(proper_divisors, n)) - ), computational_implementation=lambda n: n == sum(i for i in range(1, n) if n % i == 0), example_structure=ExampleStructure( @@ -173,7 +135,6 @@ is_even = Concept( name="is_even", description="A number divisible by 2", - symbolic_definition=lambda n: ConceptApplication(divides, Nat(2), n), computational_implementation=lambda n: n % 2 == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -185,7 +146,6 @@ is_odd = Concept( name="is_odd", description="Tests if a number is not divisible by 2", - symbolic_definition=lambda n: Not(ConceptApplication(is_even, n)), computational_implementation=lambda n: n % 2 == 1, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -197,9 +157,6 @@ leq_than = Concept( name="leq_than", description="a ≤ b if there exists m such that b = a + m", - symbolic_definition=lambda a, b: Exists( - "m", NatDomain(), Equals(b, addition(a, Var("m"))) - ), computational_implementation=lambda a, b: a <= b, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -214,7 +171,6 @@ greater_than = Concept( name="greater_than", description="a > b if not (a ≤ b)", - symbolic_definition=lambda a, b: Not(ConceptApplication(leq_than, a, b)), computational_implementation=lambda a, b: a > b, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -229,7 +185,6 @@ geq_than = Concept( name="geq_than", description="a ≥ b if not (a < b)", - symbolic_definition=lambda a, b: Not(ConceptApplication(less_than, a, b)), computational_implementation=lambda a, b: a >= b, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -244,26 +199,6 @@ gcd = Concept( name="gcd", description="Greatest common divisor - largest number that divides both inputs", - symbolic_definition=lambda a, b: Lambda( - "d", - And( - And( - ConceptApplication(divides, Var("d"), a), - ConceptApplication(divides, Var("d"), b), - ), - Forall( - "k", - NatDomain(), - Implies( - And( - ConceptApplication(divides, Var("k"), a), - ConceptApplication(divides, Var("k"), b), - ), - ConceptApplication(leq_than, Var("k"), Var("d")), - ), - ), - ), - ), computational_implementation=lambda a, b: b if a == 0 else gcd.compute(b % a, a), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -275,26 +210,6 @@ lcm = Concept( name="lcm", description="Least common multiple - smallest number divisible by both inputs", - symbolic_definition=lambda a, b: Lambda( - "l", - And( - And( - ConceptApplication(divides, a, Var("l")), - ConceptApplication(divides, b, Var("l")), - ), - Forall( - "k", - NatDomain(), - Implies( - And( - ConceptApplication(divides, a, Var("k")), - ConceptApplication(divides, b, Var("k")), - ), - ConceptApplication(leq_than, Var("l"), Var("k")), - ), - ), - ), - ), computational_implementation=lambda a, b: abs(a * b) // gcd.compute(a, b), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -312,18 +227,6 @@ infinitude_of_primes = Conjecture( name="infinitude_of_primes", description="For every natural number n, there exists a prime number greater than n", - symbolic_definition=lambda: Forall( - "n", - NatDomain(), - Exists( - "p", - NatDomain(), - And( - ConceptApplication(greater_than, Var("p"), Var("n")), - ConceptApplication(is_prime, Var("p")), - ), - ), - ), computational_implementation=lambda bound=1000: all( any(p > n and is_prime.compute(p) for p in range(n + 1, min(2 * n, bound))) for n in range(1, bound) @@ -333,21 +236,6 @@ twin_prime_conjecture = Conjecture( name="twin_prime_conjecture", description="There are infinitely many pairs of prime numbers that differ by 2", - symbolic_definition=lambda: Forall( - "n", - NatDomain(), - Exists( - "p", - NatDomain(), - And( - ConceptApplication(greater_than, Var("p"), Var("n")), - And( - ConceptApplication(is_prime, Var("p")), - ConceptApplication(is_prime, addition(Var("p"), Nat(2))), - ), - ), - ), - ), computational_implementation=lambda bound=1000: all( any( is_prime.compute(p) and is_prime.compute(p + 2) @@ -360,31 +248,6 @@ goldbach_conjecture = Conjecture( name="goldbach_conjecture", description="Every even integer greater than 2 can be expressed as the sum of two primes", - symbolic_definition=lambda: Forall( - "n", - NatDomain(), - Implies( - And( - ConceptApplication(greater_than, Var("n"), Nat(2)), - ConceptApplication(is_even, Var("n")), - ), - Exists( - "p", - NatDomain(), - Exists( - "q", - NatDomain(), - And( - And( - ConceptApplication(is_prime, Var("p")), - ConceptApplication(is_prime, Var("q")), - ), - Equals(Var("n"), addition(Var("p"), Var("q"))), - ), - ), - ), - ), - ), computational_implementation=lambda bound=1000: all( any(is_prime.compute(p) and is_prime.compute(n - p) for p in range(2, n - 1)) for n in range(4, bound, 2) @@ -399,10 +262,6 @@ set_union = Concept( name="union", description="Union of two sets (A ∪ B) = {x | x ∈ A ∨ x ∈ B}", - symbolic_definition=lambda A, B: Set( - domain=A.domain, # Assuming both sets have same domain - predicate=Lambda("x", Or(In(Var("x"), A), In(Var("x"), B))), - ), computational_implementation=lambda A, B: A.union(B), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -418,10 +277,6 @@ set_intersection = Concept( name="intersection", description="Intersection of two sets (A ∩ B) = {x | x ∈ A ∧ x ∈ B}", - symbolic_definition=lambda A, B: Set( - domain=A.domain, # Assuming both sets have same domain - predicate=Lambda("x", And(In(Var("x"), A), In(Var("x"), B))), - ), computational_implementation=lambda A, B: A.intersection(B), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -437,10 +292,6 @@ set_difference = Concept( name="difference", description="Set difference (A \\ B) = {x | x ∈ A ∧ x ∉ B}", - symbolic_definition=lambda A, B: Set( - domain=A.domain, # Assuming both sets have same domain - predicate=Lambda("x", And(In(Var("x"), A), Not(In(Var("x"), B)))), - ), computational_implementation=lambda A, B: A.difference(B), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -456,16 +307,6 @@ symmetric_difference = Concept( name="symmetric_difference", description="Symmetric difference of two sets (A △ B) = {x | (x ∈ A ∧ x ∉ B) ∨ (x ∈ B ∧ x ∉ A)}", - symbolic_definition=lambda A, B: Set( - domain=A.domain, # Assuming both sets have same domain - predicate=Lambda( - "x", - Or( - And(In(Var("x"), A), Not(In(Var("x"), B))), - And(In(Var("x"), B), Not(In(Var("x"), A))), - ), - ), - ), computational_implementation=lambda A, B: A.symmetric_difference(B), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -481,9 +322,6 @@ subset = Concept( name="subset", description="A is a subset of B (A ⊆ B) if every element of A is in B", - symbolic_definition=lambda A, B: Forall( - "x", A.domain, Implies(In(Var("x"), A), In(Var("x"), B)) - ), computational_implementation=lambda A, B: A.issubset(B), example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -499,10 +337,6 @@ power_set = Concept( name="power_set", description="Power set of A (𝒫(A)) is the set of all subsets of A", - symbolic_definition=lambda A: Set( - domain=SetDomain(), # The domain is now a set of sets - predicate=Lambda("B", ConceptApplication(subset, Var("B"), A)), - ), computational_implementation=lambda A: { frozenset(x for j, x in enumerate(A) if i & (1 << j)) for i in range(1 << len(A)) @@ -517,30 +351,6 @@ distributivity_union_over_intersection = Conjecture( name="distributivity_union_over_intersection", description="Union distributes over intersection: A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)", - symbolic_definition=lambda: Forall( - "A", - SetDomain(), - Forall( - "B", - SetDomain(), - Forall( - "C", - SetDomain(), - Equals( - ConceptApplication( - set_union, - Var("A"), - ConceptApplication(set_intersection, Var("B"), Var("C")), - ), - ConceptApplication( - set_intersection, - ConceptApplication(set_union, Var("A"), Var("B")), - ConceptApplication(set_union, Var("A"), Var("C")), - ), - ), - ), - ), - ), computational_implementation=lambda bound=10: all( A.union(B.intersection(C)) == A.union(B).intersection(A.union(C)) for A in [{i for i in range(bound)} for _ in range(3)] @@ -561,8 +371,6 @@ "For a group represented as an instance of Group, this is simply the size of its carrier." ), # Symbolically, we extract the carrier (a Set) from the group and apply SetCardinality. - symbolic_definition=lambda grp: SetCardinality(grp.carrier), - # Computationally, we evaluate the carrier to a concrete Python set and take its length. computational_implementation=lambda grp: len(grp.carrier.evaluate()), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -578,18 +386,6 @@ is_abelian = Concept( name="is_abelian", description="A group is abelian if its operation is commutative.", - symbolic_definition=lambda grp: Forall( - "a", - grp.carrier, - Forall( - "b", - grp.carrier, - Equals( - grp.op(Var("a"), Var("b")), - grp.op(Var("b"), Var("a")), - ), - ), - ), computational_implementation=lambda grp: all( grp.op(a, b) == grp.op(b, a) for a in grp.carrier.evaluate() @@ -609,11 +405,6 @@ "Conjugation of a group element x by an element g is defined as g * x * g⁻¹. " "This operation is fundamental in group theory, capturing how one element 'acts' on another." ), - # Symbolic definition: for a group 'grp', g and x in its carrier, the conjugate is: - # op(op(g, x), inverse(g)) - symbolic_definition=lambda grp, g, x: ConceptApplication( - grp.op, ConceptApplication(grp.op, g, x), ConceptApplication(grp.inverse, g) - ), # Computational implementation: perform the operation using the group's op and inverse functions. computational_implementation=lambda grp, g, x: grp.op(grp.op(g, x), grp.inverse(g)), example_structure=ExampleStructure( diff --git a/frame/knowledge_base/entities.py b/frame/knowledge_base/entities.py index 42b3fa0..4fbe713 100644 --- a/frame/knowledge_base/entities.py +++ b/frame/knowledge_base/entities.py @@ -1677,7 +1677,6 @@ def __init__( self, name: str, description: str, - symbolic_definition: callable, computational_implementation: callable, example_structure: "Optional[ExampleStructure]" = None, lean4_translation: "Optional[callable]" = None, @@ -1689,7 +1688,6 @@ def __init__( """Initialize a mathematical entity with its definitions and translations""" self.name = name self.description = description - self._symbolic = symbolic_definition self._compute = computational_implementation self._has_computational_implementation = ( computational_implementation is not None @@ -1845,10 +1843,6 @@ def remove_invalid_examples(self) -> Tuple[List[Example], List[Example]]: return (removed_examples, removed_nonexamples) - def symbolic(self, *args) -> Expression: - """Returns the raw symbolic mathematical definition""" - return self._symbolic(*args) - def compute(self, *args): """Returns the computational result""" return self._compute(*args) @@ -1882,18 +1876,6 @@ def to_z3( """Returns Z3 translation.""" return self._z3(*args) - def __call__(self, *args) -> Expression: - """Returns symbolic definition unless one of the arguments is an Entity.""" - # Check if any of the arguments is an Entity - if any(isinstance(arg, Entity) for arg in args): - # If we have nested concepts, evaluate them first - evaluated_args = [ - arg(*args) if isinstance(arg, Entity) else arg for arg in args - ] - return self.symbolic(*evaluated_args) - # Otherwise just return the symbolic definition - return self.symbolic(*args) - def set_z3_translation( self, translation: callable, @@ -1930,7 +1912,6 @@ def __eq__(self, other: "Entity") -> bool: 1. They are of the same type (both Concepts, both Conjectures, or both Theorems) 2. If they are concepts, they must have the same concept type (function/predicate) 3. If they have arities, they must match - 4. Their symbolic definitions produce identical expressions for all possible inputs """ if not isinstance(other, Entity): return NotImplemented @@ -1961,66 +1942,6 @@ def __eq__(self, other: "Entity") -> bool: ): return False - # Compare symbolic definitions - if hasattr(self, "_symbolic") and hasattr(other, "_symbolic"): - try: - # Get function signatures - if isinstance(self, Concept): - self_sig = self.get_input_arity() - other_sig = other.get_input_arity() - else: - # Fallback to co_argcount for non-Concept entities - self_sig = self._symbolic.__code__.co_argcount - other_sig = other._symbolic.__code__.co_argcount - - if self_sig != other_sig: - return False - - # Create dummy arguments for testing symbolic equality - # Test with varied inputs to catch differences - test_cases = [ - tuple(1 for _ in range(self_sig)), # All 1s - tuple(i+1 for i in range(self_sig)), # Sequential numbers - # tuple(2**i for i in range(self_sig)), # Powers of 2 - ] - - for test_idx, test_args in enumerate(test_cases): - - try: - self_expr = self.symbolic(*test_args) - except Exception as e: - continue # Try next test case instead of failing - - try: - other_expr = other.symbolic(*test_args) - except Exception as e: - continue # Try next test case instead of failing - - # Only compare if both evaluations succeeded - if self_expr != other_expr: - return False - - # If we reached here, consider them equal - # Additional safety check: ensure at least one test succeeded - successful_tests = 0 - for test_args in test_cases: - try: - self_expr = self.symbolic(*test_args) - other_expr = other.symbolic(*test_args) - if self_expr == other_expr: - successful_tests += 1 - except Exception: - continue - - # Only consider equal if at least one test passed - return successful_tests > 0 - - except Exception as e: - print(f"Unexpected error in equality check: {e}") - import traceback - traceback.print_exc() - return False - return False def __hash__(self) -> int: @@ -2047,7 +1968,6 @@ def __init__( self, name: str, description: str, - symbolic_definition: callable, computational_implementation: callable, example_structure: ExampleStructure, lean4_translation: "Optional[callable]" = None, @@ -2059,7 +1979,6 @@ def __init__( super().__init__( name, description, - symbolic_definition, computational_implementation, example_structure, lean4_translation, @@ -2084,7 +2003,6 @@ def __init__( self, name: str, description: str, - symbolic_definition: callable, example_structure: "Optional[ExampleStructure]" = None, lean4_translation: "Optional[callable]" = None, prolog_translation: "Optional[callable]" = None, @@ -2100,7 +2018,6 @@ def __init__( super().__init__( name, description, - symbolic_definition, computational_implementation, example_structure, lean4_translation, @@ -2135,7 +2052,6 @@ def __init__( self, name: str, description: str, - symbolic_definition: callable, proof: Proof, example_structure: "Optional[ExampleStructure]" = None, lean4_translation: "Optional[callable]" = None, @@ -2148,7 +2064,6 @@ def __init__( super().__init__( name=name, description=description, - symbolic_definition=symbolic_definition, computational_implementation=computational_implementation, example_structure=example_structure, lean4_translation=lean4_translation, diff --git a/frame/knowledge_base/initial_concepts.py b/frame/knowledge_base/initial_concepts.py index 7fd8daf..586dd57 100644 --- a/frame/knowledge_base/initial_concepts.py +++ b/frame/knowledge_base/initial_concepts.py @@ -15,7 +15,6 @@ def create_successor_concept(): succ = Concept( name="successor", description="The successor function n -> n+1", - symbolic_definition=lambda n: Succ(n), computational_implementation=lambda n: n + 1, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -55,7 +54,6 @@ def create_zero_concept(): zero = Concept( name="zero", description="The constant zero", - symbolic_definition=lambda: Zero(), computational_implementation=lambda: 0, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -86,7 +84,6 @@ def create_one_concept(): one = Concept( name="one", description="The constant one", - symbolic_definition=lambda: Succ(Zero()), computational_implementation=lambda: 1, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -116,7 +113,6 @@ def create_two_concept(): two = Concept( name="two", description="The constant two", - symbolic_definition=lambda: Succ(Succ(Zero())), computational_implementation=lambda: 2, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -148,7 +144,6 @@ def create_addition_concept(): add = Concept( name="add", description="Addition of natural numbers defined by repeated succession", - symbolic_definition=lambda a, b: Fold(b, a, Lambda("x", Succ(Var("x")))), computational_implementation=lambda a, b: a + b, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -195,9 +190,6 @@ def create_multiplication_concept(): mult = Concept( name="multiply", description="Multiplication of natural numbers defined by repeated addition", - symbolic_definition=lambda a, b: Fold( - b, Zero(), Lambda("x", ConceptApplication(addition_concept, Var("x"), a)) - ), computational_implementation=lambda a, b: a * b, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -242,9 +234,6 @@ def create_divides_concept(): div = Concept( name="divides", description="a divides b if there exists n such that b = a*n", - symbolic_definition=lambda a, b: Exists( - "n", NatDomain(), Equals(b, ConceptApplication(multiplication_concept, a, Var("n"))) - ), computational_implementation=lambda a, b: (a == 0 and b == 0) or (a != 0 and b % a == 0), example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -286,9 +275,6 @@ def create_leq_than_concept(): leq = Concept( name="leq_than", description="a ≤ b if there exists m such that b = a + m", - symbolic_definition=lambda a, b: Exists( - "m", NatDomain(), Equals(b, ConceptApplication(addition_concept, a, Var("m"))) - ), computational_implementation=lambda a, b: a <= b, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -332,7 +318,6 @@ def create_equality_concept(): eq = Concept( name="eq", description="a equals b", - symbolic_definition=lambda a, b: Equals(a, b), computational_implementation=lambda a, b: a == b, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, diff --git a/frame/knowledge_base/knowledge_graph.py b/frame/knowledge_base/knowledge_graph.py index f40f91c..c8e9ddb 100644 --- a/frame/knowledge_base/knowledge_graph.py +++ b/frame/knowledge_base/knowledge_graph.py @@ -13,8 +13,6 @@ from dataclasses import dataclass from graphviz import Digraph import os -import json -import pickle import dill import logging diff --git a/frame/productions/concepts/compose.py b/frame/productions/concepts/compose.py index 54e9b75..97139f3 100644 --- a/frame/productions/concepts/compose.py +++ b/frame/productions/concepts/compose.py @@ -657,10 +657,6 @@ def _translation(*args, inner_function, outer_function): return None return outer_function(*outer_args) - - def symbolic_definition(*args): - """Build function composition""" - return _translation(*args, inner_function=inner.symbolic, outer_function=outer.symbolic) def compute(*args): """Compute composition""" @@ -741,7 +737,6 @@ def _z3_translate_compose_functions(*args): new_concept = Concept( name=f"compose_({inner.name}_with_{outer.name}_output_to_input_map={output_to_input_map})", description=f"Function composition of {inner.name} and {outer.name}", - symbolic_definition=symbolic_definition, computational_implementation=compute if inner.has_computational_implementation() and outer.has_computational_implementation() @@ -771,7 +766,6 @@ def _compose_predicates( def _translation(*args, pred1_function, pred2_function, shared_vars): """Build conjunction of predicates with shared variables""" - # Similar logic to symbolic_definition args1 = [None] * arity1 args2 = [None] * arity2 @@ -807,15 +801,6 @@ def _translation(*args, pred1_function, pred2_function, shared_vars): # or returns a non-callable value return None - def symbolic_definition(*args): - """Build conjunction of predicates with shared variables""" - result1, result2 = _translation(*args, - pred1_function=pred1.symbolic, - pred2_function=pred2.symbolic, - shared_vars=shared_vars) - - return And(result1, result2) - def compute(*args): """Compute conjunction of predicates""" result1, result2 = _translation(*args, @@ -917,7 +902,6 @@ def _z3_translate_compose_predicates(*args): new_concept = Concept( name=f"compose_({pred1.name}_with_{pred2.name}_shared_vars={shared_vars})", description=f"Predicate composition of {pred1.name} and {pred2.name}", - symbolic_definition=symbolic_definition, computational_implementation=compute if pred1.has_computational_implementation() and pred2.has_computational_implementation() @@ -976,11 +960,6 @@ def _translation(*args, func_function, pred_function): return pred_function(*pred_args) - - def symbolic_definition(*args): - """Build predicate from function application""" - return _translation(*args, func_function=func.symbolic, pred_function=pred.symbolic) - def compute(*args): """Compute by applying function then predicate""" return _translation(*args, func_function=func.compute, pred_function=pred.compute) @@ -1052,7 +1031,6 @@ def _z3_translate_compose_function_to_predicate(*args): new_concept = Concept( name=f"compose_({func.name}_with_{pred.name}_output_to_input_map={output_to_input_map})", description=f"Function-to-predicate composition of {func.name} and {pred.name}", - symbolic_definition=symbolic_definition, computational_implementation=compute if func.has_computational_implementation() and pred.has_computational_implementation() diff --git a/frame/productions/concepts/constant.py b/frame/productions/concepts/constant.py index 4c27aa5..a9302b2 100644 --- a/frame/productions/concepts/constant.py +++ b/frame/productions/concepts/constant.py @@ -232,9 +232,6 @@ def constant_compute(): new_concept = Concept( name=f"constant_({constant_value}_from_{concept.name})", description=f"Constant value {constant_value} derived from {concept.name}", - # Symbolic definition should ideally use a proper Constant entity if available - # For now, using the value directly might suffice for simple cases - symbolic_definition=lambda val=constant_value: val, computational_implementation=constant_compute, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, diff --git a/frame/productions/concepts/exists.py b/frame/productions/concepts/exists.py index dd42544..360f753 100644 --- a/frame/productions/concepts/exists.py +++ b/frame/productions/concepts/exists.py @@ -49,9 +49,8 @@ class ExistsRule(ProductionRule): The rule: 1. Takes a concept and indices of arguments to quantify over - 2. Creates new symbolic definition with existential quantifiers - 3. Creates computational implementation that searches for witnesses - 4. Transforms examples based on existence of witnesses + 2. Creates computational implementation that searches for witnesses + 3. Transforms examples based on existence of witnesses """ def __init__(self, internal_search_timeout: float = DEFAULT_INTERNAL_EXISTS_SEARCH_TIMEOUT): @@ -300,9 +299,6 @@ def apply(self, *inputs: Entity, indices_to_quantify: List[int]) -> Entity: new_concept = Concept( name=f"exists_({concept.name}_indices_{indices_to_quantify})", description=f"Existential quantification over {concept.name}", - symbolic_definition=lambda *args: self._build_exists_expr( - concept, args, indices_to_quantify, is_function - ), computational_implementation=self._build_computational_impl( concept, indices_to_quantify, is_function ), @@ -453,74 +449,6 @@ def _transform_examples(self, new_concept: Entity, concept: Entity): except Exception as e: print(f"Failed to add example: {str(e)}") - def _build_exists_expr( - self, - concept: Concept, - args: Tuple[Any, ...], - indices_to_quantify: List[int], - is_function: bool = False, - ) -> Expression: - """Build symbolic expression with existential quantifiers. - - For functions f(x1,...,xn) = (y1,...,ym), we have: - 1. Quantify over some inputs: Creates predicate P(...,y1,...,ym) = ∃xi. f(...,xi,...) = (y1,...,ym) - - For predicates P(x1,...,xn), we have: - 1. Quantify over some inputs: Creates predicate Q(...) = ∃xi. P(...,xi,...) - """ - if is_function: - # For functions, build exists k1,k2,.... f(k1,k2,...) = (y1,...,ym) - # First create the inner equality expression - inner_args = [] - arg_idx = 0 - num_inputs = concept.get_input_arity() - num_outputs = len(concept.get_component_types()) - num_inputs - - # Build argument list, using Vars for quantified indices - for i in range(num_inputs): - if i in indices_to_quantify: - inner_args.append(Var(f"k{i}")) - else: - inner_args.append(args[arg_idx]) - arg_idx += 1 - - # Get output arguments (last num_outputs arguments from args) - outputs = args[-num_outputs:] - - # Build equality: f(k1,k2,...) = (y1,...,ym) - inner_expr = Equals( - ConceptApplication(concept, *inner_args), - outputs[0] if num_outputs == 1 else outputs, - ) - - # Wrap with existential quantifiers - expr = inner_expr - for i in reversed(indices_to_quantify): - expr = Exists(f"k{i}", NatDomain(), expr) - return expr - - else: - # For predicates, use original logic - arg_map = {} - arg_idx = 0 - for i in range(concept.get_input_arity()): - if i not in indices_to_quantify: - arg_map[i] = args[arg_idx] - arg_idx += 1 - - inner_args = [] - for i in range(concept.get_input_arity()): - if i in indices_to_quantify: - inner_args.append(Var(f"y{i}")) - else: - inner_args.append(arg_map[i]) - inner_expr = ConceptApplication(concept, *inner_args) - - expr = inner_expr - for i in reversed(indices_to_quantify): - expr = Exists(f"y{i}", NatDomain(), expr) - return expr - def _build_computational_impl( self, concept: Concept, diff --git a/frame/productions/concepts/forall.py b/frame/productions/concepts/forall.py index ba5e525..f95e9dc 100644 --- a/frame/productions/concepts/forall.py +++ b/frame/productions/concepts/forall.py @@ -566,9 +566,6 @@ def _apply_single_predicate( new_concept = Concept( name=f"forall_({concept.name}_indices_to_quantify_{indices_to_quantify})", description=f"Universal quantification over {concept.name}", - symbolic_definition=lambda *args: self._build_single_forall_expr( - concept, args, indices_to_quantify, kept_indices#, domains - ), computational_implementation=self._build_computational_impl( concept, indices=indices_to_quantify, @@ -630,7 +627,6 @@ def _apply_single_predicate( new_conjecture = Conjecture( name=f"forall_({concept.name}_indices_to_quantify_{indices_to_quantify})", description=f"Universal quantification conjecture over {concept.name}", - symbolic_definition=lambda: expr, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, component_types=(), @@ -819,11 +815,6 @@ def _apply_two_predicates( self.determine_verification_capabilities(primary, secondary) ) - # 5. Build Symbolic Definition - symbolic_definition_lambda = self._build_symbolic_definition_two_pred( - primary, secondary, var_info, quantified_var_ids, parameter_var_ids, is_conjecture - ) - # 6. Build Computational Implementation computational_impl_lambda = self._build_computational_impl_two_pred( primary, secondary, var_info, quantified_var_ids, parameter_var_ids @@ -837,7 +828,6 @@ def _apply_two_predicates( new_entity = Conjecture( name=name, description=description, - symbolic_definition=symbolic_definition_lambda, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, component_types=(), @@ -856,7 +846,6 @@ def _apply_two_predicates( new_entity = Concept( name=name, description=description, - symbolic_definition=symbolic_definition_lambda, computational_implementation=computational_impl_lambda, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -984,102 +973,6 @@ def _z3_translate_forall_two_predicates( template.set_args(*args) return template - - def _build_single_forall_expr( - self, - concept: Concept, - args: Tuple[Any, ...], - indices: List[int], - kept_indices: List[int], - # domains: List[Entity], - ) -> Expression: - """Build symbolic expression with universal quantifiers for a single predicate.""" - # Map the unquantified (kept) arguments to their positions - arg_map = {} - for i, kept_idx in enumerate(kept_indices): - arg_map[kept_idx] = args[i] - - # Build the predicate arguments - concept_args = [] - for i in range(concept.get_input_arity()): - if i in indices: - # Use Var for quantified indices - concept_args.append(Var(f"x{i}")) - else: - # Use the actual argument for unquantified indices - concept_args.append(arg_map[i]) - - # Create the inner expression: P(...) - expr = ConceptApplication(concept, *concept_args) - - # Wrap with universal quantifiers (starting from the innermost) - for i, idx in enumerate(reversed(indices)): - domain_idx = len(indices) - i - 1 # Adjust for reversed order - expr = Forall(f"x{idx}", NatDomain(), expr) - - return expr - - def _build_symbolic_definition_two_pred( - self, - primary: Concept, - secondary: Concept, - var_info: Dict[str, Dict[str, Any]], - quantified_var_ids: set[str], - parameter_var_ids: List[str], - is_conjecture: bool - ) -> callable: - """Builds the symbolic definition lambda for the two-predicate case.""" - - def build_expression(*param_values): - # Create argument lists for P and Q applications - primary_args = [None] * primary.get_input_arity() - secondary_args = [None] * secondary.get_input_arity() - value_map = {} # Maps var_id to Var obj or parameter value - - # Populate value_map with parameter values first - for i, var_id in enumerate(parameter_var_ids): - value_map[var_id] = param_values[i] - - # Populate value_map with Var objects for quantified/shared vars - # And build argument lists - for var_id, info in var_info.items(): - if var_id not in value_map: # Quantified or shared - value_map[var_id] = info["var_obj"] - - # Assign to primary_args if applicable - if "primary_idx" in info: - primary_args[info["primary_idx"]] = value_map[var_id] - - # Assign to secondary_args if applicable - if "secondary_idx" in info: - secondary_args[info["secondary_idx"]] = value_map[var_id] - - # Create the core implication P(...) => Q(...) - antecedent = ConceptApplication(primary, *primary_args) - consequent = ConceptApplication(secondary, *secondary_args) - implication = Implies(antecedent, consequent) - - # Wrap with Forall quantifiers - expr = implication - quantified_vars_ordered = sorted(list(quantified_var_ids)) # Consistent order - quantified_types = [var_info[vid]["type"] for vid in quantified_vars_ordered] - # domains = self._infer_domains(quantified_types) - - for i, var_id in enumerate(reversed(quantified_vars_ordered)): - var_obj = var_info[var_id]["var_obj"] - domain = NatDomain() - expr = Forall(var_obj.name, domain, expr) # Use var_obj.name for consistency - - return expr - - if is_conjecture: - # For conjectures, build the expression immediately - static_expr = build_expression() - return lambda: static_expr - else: - # For concepts, return the function that takes params and builds expression - return build_expression - def _build_computational_impl_two_pred( self, primary: Concept, diff --git a/frame/productions/concepts/map_iterate.py b/frame/productions/concepts/map_iterate.py index 9ccdd1d..22c556b 100644 --- a/frame/productions/concepts/map_iterate.py +++ b/frame/productions/concepts/map_iterate.py @@ -309,18 +309,6 @@ def iterate_compute(a, n): else f"iterate_({base_concept.name}_with_{inputs[1].name})" ), description=f"Applies {base_concept.name} iteratively", - symbolic_definition=lambda a, n: Fold( - n, # Number of iterations - inputs[1].symbolic() if is_binary else a, # Starting value - Lambda( - "x", - ( - ConceptApplication(base_concept, a, Var("x")) - if is_binary - else ConceptApplication(base_concept, Var("x")) - ), - ), # Step function - ), computational_implementation=iterate_compute, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, diff --git a/frame/productions/concepts/match.py b/frame/productions/concepts/match.py index 7bf0f49..bee201e 100644 --- a/frame/productions/concepts/match.py +++ b/frame/productions/concepts/match.py @@ -29,9 +29,8 @@ class MatchRule(ProductionRule): The rule: 1. Takes a concept and indices of arguments to match - 2. Creates new symbolic definition where specified arguments are the same - 3. Creates computational implementation that passes the same value to matched arguments - 4. Transforms examples by filtering for cases where specified arguments are equal + 2. Creates computational implementation that passes the same value to matched arguments + 3. Transforms examples by filtering for cases where specified arguments are equal """ def __init__(self): @@ -302,12 +301,6 @@ def _z3_translate_match(*args): new_concept = Concept( name=f"matched_({concept.name}_indices_{indices_to_match})", description=f"Specialization of {concept.name} with arguments {indices_to_match} made equal", - symbolic_definition=lambda *args: ConceptApplication( - concept, - *[ - args[old_to_new[i]] for i in range(input_arity) - ], # Only use input indices - ), computational_implementation=matched_compute if concept.has_computational_implementation() else None, diff --git a/frame/productions/concepts/negate.py b/frame/productions/concepts/negate.py index 050f9e8..20f81bd 100644 --- a/frame/productions/concepts/negate.py +++ b/frame/productions/concepts/negate.py @@ -143,7 +143,6 @@ def negate_compute(*args): new_concept = Concept( name=f"not_({concept.name})", description=f"Negation of {concept.name}", - symbolic_definition=lambda *args: Not(ConceptApplication(concept, *args)), computational_implementation=( negate_compute if concept.has_computational_implementation() else None ), diff --git a/frame/productions/concepts/size.py b/frame/productions/concepts/size.py index 2e3fedb..c8194e9 100644 --- a/frame/productions/concepts/size.py +++ b/frame/productions/concepts/size.py @@ -223,9 +223,6 @@ def size_compute(*args): new_concept = Concept( name=f"size_of_({concept.name}_indices_{indices_to_quantify})", description=f"Cardinality of the set returned by {concept.name}", - symbolic_definition=lambda *args: ConceptApplication( - SetCardinality, ConceptApplication(concept, *args) - ), computational_implementation=size_compute, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -270,26 +267,6 @@ def size_compute(*args): else: default_domain = TupleDomain(tuple(domains)) - def symbolic_definition(*args): - # args corresponds to free argument translations. - free_args = list(args) - full_args = [] - free_index = 0 - for i in range(input_arity): - if i in indices_to_quantify: - # Insert the corresponding bound variable. - full_args.append(bound_vars[indices_to_quantify.index(i)]) - else: - full_args.append(free_args[free_index]) - free_index += 1 - pred_expr = ConceptApplication(concept, *full_args) - # Build nested lambda abstraction recursively over the bound variables. - lam = pred_expr - for var in reversed(bound_vars): - lam = Lambda(var, lam) - set_expr = Set(domain=default_domain, predicate=lam) - return ConceptApplication(SetCardinality, set_expr) - # New component types: free argument types plus NUMERIC output. new_comp_types = [comp_types[i] for i in free_indices] + [ExampleType.NUMERIC] @@ -298,7 +275,6 @@ def symbolic_definition(*args): description=( f"Cardinality of the set of values for arguments {indices_to_quantify} satisfying {concept.name}" ), - symbolic_definition=symbolic_definition, computational_implementation=None, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, diff --git a/frame/productions/concepts/specialize.py b/frame/productions/concepts/specialize.py index 3936cfe..781c972 100644 --- a/frame/productions/concepts/specialize.py +++ b/frame/productions/concepts/specialize.py @@ -405,9 +405,6 @@ def _z3_output_specialized(*args): return Concept( name=f"specialized_({concept.name}_output_eq_{value_name})", description=f"Specialization of {concept.name} checking if output equals {fixed_value}", - symbolic_definition=lambda *args: Equals( - ConceptApplication(concept, *args), Nat(fixed_value) - ), computational_implementation=lambda *args: ( _compute_output_specialized(concept, *args) if concept.has_computational_implementation() @@ -469,13 +466,6 @@ def _create_input_specialized_concept( else: component_types = tuple(component_types) - def specialized_input_symbolic(*args): - """Create symbolic definition with fixed value""" - symbolic_args = list(args) - # We assume the fixed value needs wrapping for the symbolic representation - symbolic_args.insert(index_to_specialize, Nat(fixed_value)) - return ConceptApplication(concept, *symbolic_args) - def specialized_input_compute(*args): """Insert fixed value at specialized index""" full_args = list(args) @@ -486,7 +476,6 @@ def specialized_input_compute(*args): return Concept( name=f"specialized_({concept.name}_at_{index_to_specialize}_to_{value_name})", description=f"Specialization of {concept.name} with argument {index_to_specialize} fixed to {fixed_value}", - symbolic_definition=specialized_input_symbolic, computational_implementation=( specialized_input_compute if concept.has_computational_implementation() diff --git a/frame/productions/conjectures/equivalence.py b/frame/productions/conjectures/equivalence.py index 955f638..26cffe1 100644 --- a/frame/productions/conjectures/equivalence.py +++ b/frame/productions/conjectures/equivalence.py @@ -273,7 +273,6 @@ def apply(self, *inputs: Entity) -> Entity: conjecture = Conjecture( name=f"equiv_({concept1.name}_{concept2.name})", description=f"Conjecture that {concept1.name} and {concept2.name} are equivalent", - symbolic_definition=lambda: expr, example_structure=concept1.examples.example_structure, can_add_examples=can_add_examples, can_add_nonexamples=can_add_nonexamples, @@ -291,13 +290,6 @@ def create_subtraction_concept(): concept = Concept( name="subtraction", description="Subtraction of natural numbers (returns 0 if result would be negative)", - symbolic_definition=lambda a, b: - Exists("k", NatDomain(), - And( - ConceptApplication(addition, b, Var("k")), - Equals(Var("k"), a) - ) - ), computational_implementation=lambda a, b: max(0, a - b), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -322,8 +314,6 @@ def create_power_concept(): concept = Concept( name="power", description="Power function a^n defined by repeated multiplication", - symbolic_definition=lambda a, n: - Fold(n, one_concept.symbolic(), Lambda("x", multiplication(Var("x"), a))), computational_implementation=lambda a, n: a ** n, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -350,30 +340,6 @@ def create_mersenne_form_concept(): concept = Concept( name="is_mersenne_form", description="Tests if n is of the form 2^k * (2^(k+1) - 1) where 2^(k+1) - 1 is prime", - symbolic_definition=lambda n: - Exists("k", NatDomain(), - And( - ConceptApplication(is_prime, - ConceptApplication(subtraction, - ConceptApplication(power, Nat(2), - ConceptApplication(addition, Var("k"), Nat(1)) - ), - Nat(1) - ) - ), - Equals(n, - ConceptApplication(multiplication, - ConceptApplication(power, Nat(2), Var("k")), - ConceptApplication(subtraction, - ConceptApplication(power, Nat(2), - ConceptApplication(addition, Var("k"), Nat(1)) - ), - Nat(1) - ) - ) - ) - ) - ), computational_implementation=lambda n: any( is_prime.compute(2**(k+1) - 1) and @@ -410,7 +376,6 @@ def create_add1_concept(): concept = Concept( name="add1", description="Add 1 to a natural number", - symbolic_definition=lambda n: Lambda("x", addition(Var("x"), Succ(Zero()))), computational_implementation=lambda n: n + 1, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -438,11 +403,6 @@ def test_equivalence(): even_perfect = Concept( name="is_even_perfect", description="Tests if n is an even perfect number", - symbolic_definition=lambda n: - And( - ConceptApplication(is_even, n), - ConceptApplication(is_perfect, n) - ), computational_implementation=lambda n: is_even.compute(n) and is_perfect.compute(n), example_structure=ExampleStructure( @@ -485,10 +445,7 @@ def test_equivalence(): if can_apply: print("\nApplying rule to create predicate conjecture...") conjecture = equivalence.apply(even_perfect, mersenne_form) - - # Show symbolic form - print("\nSymbolic form of conjecture:") - symbolic_expr = conjecture.symbolic() + # Test function equivalence @@ -499,8 +456,6 @@ def test_equivalence(): if can_apply: print("\nApplying rule to create function conjecture...") conjecture = equivalence.apply(add1, successor) - print("\nSymbolic form of function conjecture:") - symbolic_expr = conjecture.symbolic() return conjecture @@ -516,7 +471,6 @@ def create_is_even_concept_z3(): concept = Concept( name="is_even_z3", description="Tests if a number is even (Z3)", - symbolic_definition=lambda n: n % 2 == 0, # Simplified for testing computational_implementation=lambda n: n % 2 == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -538,7 +492,6 @@ def create_is_square_concept_z3(): concept = Concept( name="is_square_z3", description="Tests if a number is a perfect square (Z3)", - symbolic_definition=lambda n: Exists("k", NatDomain(), Equals(n, ConceptApplication(multiplication, Var("k"), Var("k")))), computational_implementation=lambda n: n >= 0 and int(n**0.5)**2 == n, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -565,7 +518,6 @@ def create_is_even_square_concept_z3(): concept = Concept( name="is_even_square_z3", description="Tests if a number's square is an even number (Z3)", - symbolic_definition=lambda n: And(ConceptApplication(is_even_c, n), ConceptApplication(is_square_c, n)), computational_implementation=lambda n: (n % 2 == 0) and (n >= 0 and int(n**0.5)**2 == n), example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -590,7 +542,6 @@ def create_divisible_by_4_concept_z3(): concept = Concept( name="is_divisible_by_4_z3", description="Tests if a number is divisible by 4 (Z3)", - symbolic_definition=lambda n: ConceptApplication(divides, Nat(4), n), computational_implementation=lambda n: n % 4 == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -611,7 +562,6 @@ def create_double_concept_z3(): concept = Concept( name="double_z3", description="Multiplies input by 2 (Z3)", - symbolic_definition=lambda x: ConceptApplication(multiplication, Nat(2), x), computational_implementation=lambda x: 2 * x, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -632,7 +582,6 @@ def create_add_self_concept_z3(): concept = Concept( name="add_self_z3", description="Adds input to itself (Z3)", - symbolic_definition=lambda x: ConceptApplication(addition, x, x), computational_implementation=lambda x: x + x, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -653,7 +602,6 @@ def create_add_two_concept_z3(): concept = Concept( name="add_two_z3", description="Adds 2 to input (Z3)", - symbolic_definition=lambda x: ConceptApplication(addition, x, Nat(2)), computational_implementation=lambda x: x + 2, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, diff --git a/frame/productions/conjectures/exclusivity.py b/frame/productions/conjectures/exclusivity.py index f765ee1..670dcf1 100644 --- a/frame/productions/conjectures/exclusivity.py +++ b/frame/productions/conjectures/exclusivity.py @@ -232,7 +232,6 @@ def apply(self, *inputs: Entity, valid_set: Optional[Set] = None, target_value: conjecture = Conjecture( name=f"excl_({concept.name}{name_suffix}_{valid_set})", description=f"Conjecture that '{concept.name}' is satisfied exactly on the set {valid_set}", - symbolic_definition=lambda: expr, example_structure=concept.examples.example_structure, can_add_examples=can_add_examples, can_add_nonexamples=can_add_nonexamples @@ -246,10 +245,6 @@ def create_even_prime_concept(): concept = Concept( name="is_even_prime", description="Tests if a number is both even and prime", - symbolic_definition=lambda n: And( - ConceptApplication(is_even, n), - ConceptApplication(is_prime, n) - ), computational_implementation=lambda n: is_even.compute(n) and is_prime.compute(n), example_structure=ExampleStructure( @@ -277,9 +272,6 @@ def create_sum_equals_concept(): concept = Concept( name="sum_equals_4", description="Tests if two numbers sum to 4", - symbolic_definition=lambda x, y: Equals( - ConceptApplication(addition, x, y), Nat(4) - ), computational_implementation=lambda x, y: x + y == 4, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -323,10 +315,7 @@ def test_exclusivity(): if can_apply: print("\nApplying rule to create excl_even_prime_numbers conjecture...") excl_even_prime = exclusivity.apply(even_prime, valid_set={(2,)}) - - # Show symbolic form - print("\nSymbolic form of conjecture:") - symbolic_expr = excl_even_prime.symbolic() + # Test 2: Pairs of numbers that sum to 4 @@ -347,9 +336,6 @@ def test_exclusivity(): print("\nApplying rule to create excl_sum_equals_4 conjecture...") excl_sum_equals_4 = exclusivity.apply(sum_equals_4, valid_set=valid_pairs) - # Show symbolic form - print("\nSymbolic form of conjecture:") - symbolic_expr = excl_sum_equals_4.symbolic() return excl_even_prime, excl_sum_equals_4 diff --git a/frame/productions/conjectures/implication.py b/frame/productions/conjectures/implication.py index f508258..c654151 100644 --- a/frame/productions/conjectures/implication.py +++ b/frame/productions/conjectures/implication.py @@ -225,7 +225,6 @@ def apply(self, *inputs: Entity) -> Entity: conjecture = Conjecture( name=f"implies_({concept1.name}_{concept2.name})", description=f"Conjecture that {concept1.name} implies {concept2.name}", - symbolic_definition=lambda: expr, example_structure=concept1.examples.example_structure, can_add_examples=can_add_examples, can_add_nonexamples=can_add_nonexamples, @@ -278,7 +277,6 @@ def create_divisible_by_4_concept(): concept = Concept( name="is_divisible_by_4", description="Tests if a number is divisible by 4", - symbolic_definition=lambda n: ConceptApplication(divides, Nat(4), n), computational_implementation=lambda n: n % 4 == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -311,10 +309,6 @@ def create_even_square_concept(): square = Concept( name="is_square", description="Tests if a number is a perfect square", - symbolic_definition=lambda n: - Exists("k", NatDomain(), - Equals(n, ConceptApplication(multiplication, Var("k"), Var("k"))) - ), computational_implementation=lambda n: int(n ** 0.5) ** 2 == n, example_structure=ExampleStructure( @@ -344,10 +338,6 @@ def create_even_square_concept(): concept = Concept( name="is_even_square", description="Tests if a number is both even and a perfect square", - symbolic_definition=lambda n: And( - ConceptApplication(is_even, n), - ConceptApplication(square, n) - ), computational_implementation=lambda n: n % 2 == 0 and int(n ** 0.5) ** 2 == n, example_structure=ExampleStructure( @@ -406,10 +396,6 @@ def test_implication(): print("\nApplying rule to create conjecture...") conjecture = implication.apply(even_square, div_by_4) - # Show symbolic form - print("\nSymbolic form of conjecture:") - symbolic_expr = conjecture.symbolic() - return conjecture return None @@ -423,7 +409,6 @@ def test_implication_z3(): is_even = Concept( name="is_even", description="Tests if a number is even", - symbolic_definition=lambda n: n % 2 == 0, computational_implementation=lambda n: n % 2 == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -449,7 +434,6 @@ def test_implication_z3(): is_divisible_by_4 = Concept( name="is_divisible_by_4", description="Tests if a number is divisible by 4", - symbolic_definition=lambda n: n % 4 == 0, computational_implementation=lambda n: n % 4 == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, diff --git a/frame/productions/conjectures/nonexistence.py b/frame/productions/conjectures/nonexistence.py index ff6365b..98cd9b6 100644 --- a/frame/productions/conjectures/nonexistence.py +++ b/frame/productions/conjectures/nonexistence.py @@ -268,7 +268,6 @@ def apply(self, *inputs: Entity) -> Entity: conjecture = Conjecture( name=f"no_({concept.name}{name_suffix})", description=f"Conjecture that no inputs to {concept.name} equal {target_concept.name if target_concept else ''}", - symbolic_definition=lambda: expr, example_structure=concept.examples.example_structure, can_add_examples=can_add_examples, can_add_nonexamples=can_add_nonexamples, @@ -337,10 +336,6 @@ def create_odd_perfect_concept(): concept = Concept( name="is_odd_perfect", description="Tests if a number is both odd and perfect", - symbolic_definition=lambda n: And( - ConceptApplication(is_odd, n), - ConceptApplication(is_perfect, n) - ), computational_implementation=lambda n: is_odd.compute(n) and is_perfect.compute(n), example_structure=ExampleStructure( @@ -365,12 +360,6 @@ def create_prime_square_concept(): concept = Concept( name="is_prime_square", description="Tests if a number is both prime and a perfect square", - symbolic_definition=lambda n: And( - ConceptApplication(is_prime, n), - Exists("k", NatDomain(), - Equals(n, ConceptApplication(multiplication, Var("k"), Var("k"))) - ) - ), computational_implementation=lambda n: is_prime.compute(n) and int(n ** 0.5) ** 2 == n, example_structure=ExampleStructure( @@ -396,7 +385,6 @@ def create_function_concept(): concept = Concept( name="add_one", description="Adds 1 to a number", - symbolic_definition=lambda n: ConceptApplication(addition, n, Nat(1)), computational_implementation=lambda n: n + 1, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -426,7 +414,6 @@ def create_constant_concept(value, name=None): concept = Concept( name=name, description=f"Constant function that always returns {value}", - symbolic_definition=lambda: Nat(value), computational_implementation=lambda: value, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -480,9 +467,6 @@ def test_nonexistence(): print("\nApplying rule to create no_odd_perfect_numbers conjecture...") no_odd_perfect = nonexistence.apply(odd_perfect) - # Show symbolic form - print("\nSymbolic form of conjecture:") - symbolic_expr = no_odd_perfect.symbolic() # Test 2: No prime square numbers (predicate case) @@ -505,10 +489,7 @@ def test_nonexistence(): print("\nApplying rule to create no_prime_squares conjecture...") no_prime_squares = nonexistence.apply(prime_square) - # Show symbolic form - print("\nSymbolic form of conjecture:") - symbolic_expr = no_prime_squares.symbolic() - + # Test 3: Function case - no number maps to 0 when add_one is applied @@ -537,10 +518,6 @@ def test_nonexistence(): print(f"\nApplying rule to create no_add_one_equals_zero conjecture...") no_add_one_equals_0 = nonexistence.apply(add_one, zero_concept) - # Show symbolic form - print("\nSymbolic form of conjecture:") - symbolic_expr = no_add_one_equals_0.symbolic() - return no_odd_perfect, no_prime_squares, no_add_one_equals_0 @@ -558,7 +535,6 @@ def test_nonexistence(): square_concept = Concept( name="square_local", description="Square a number", - symbolic_definition=lambda x: ConceptApplication(multiplication, x, x), computational_implementation=lambda x: x * x, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -631,7 +607,6 @@ def test_nonexistence(): less_than_zero_concept = Concept( name="less_than_zero", description="Tests if a number is less than 0", - symbolic_definition=lambda n: Forall(), # placeholder computational_implementation=lambda n: n < 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, diff --git a/scripts/all_zero_100_episodes.sh b/scripts/all_zero_100_episodes.sh index 86fd1d4..7ef0b41 100755 --- a/scripts/all_zero_100_episodes.sh +++ b/scripts/all_zero_100_episodes.sh @@ -9,8 +9,8 @@ cd "$(dirname "$0")/.." # Run the experiment with the standard policy config python -m frame.theory_builder \ --config-name succ_zero_standard_experiment \ - experiment.num_episodes=64 \ - experiment.max_steps=1000 \ + experiment.num_episodes=1 \ + experiment.max_steps=100 \ experiment.episode_timeout_seconds=120 \ experiment.num_workers=64 \ z3_usage.use_z3_prover=true \ diff --git a/tests/interestingness/test_hr_interestingness.py b/tests/interestingness/test_hr_interestingness.py index a648e5e..c17d8dd 100644 --- a/tests/interestingness/test_hr_interestingness.py +++ b/tests/interestingness/test_hr_interestingness.py @@ -159,7 +159,6 @@ def create_simple_test_graph(): is_negative = Concept( name="is_negative", description="Represents negative numbers", - symbolic_definition=lambda x: x < 0, computational_implementation=lambda x: x < 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, diff --git a/tests/interestingness/test_interestingness_loading.py b/tests/interestingness/test_interestingness_loading.py index 2b81de0..dd62a01 100644 --- a/tests/interestingness/test_interestingness_loading.py +++ b/tests/interestingness/test_interestingness_loading.py @@ -40,7 +40,6 @@ def setUp(self): self.concept = Concept( name="TestConcept", description="A test concept", - symbolic_definition=lambda: Zero(), computational_implementation=lambda: 0, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -54,7 +53,6 @@ def setUp(self): self.conjecture = Conjecture( name="TestConjecture", description="A test conjecture", - symbolic_definition=lambda: Zero(), # Simple placeholder computational_implementation=lambda: True, # Simple placeholder example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, diff --git a/tests/productions/conftest.py b/tests/productions/conftest.py index bcd8410..62e03cc 100644 --- a/tests/productions/conftest.py +++ b/tests/productions/conftest.py @@ -40,7 +40,6 @@ def square(): concept = Concept( name="square", description="Square a number", - symbolic_definition=lambda x: ConceptApplication(multiplication, x, x), computational_implementation=lambda x: x * x, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -71,11 +70,6 @@ def is_square(): concept = Concept( name="is_square", description="Test if a number is a perfect square", - symbolic_definition=lambda n: Exists( - "k", - NatDomain(), - Equals(n, ConceptApplication(multiplication, Var("k"), Var("k"))), - ), computational_implementation=lambda n: int(n**0.5) ** 2 == n, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -109,7 +103,6 @@ def is_even(): concept = Concept( name="is_even", description="A number divisible by 2", - symbolic_definition=lambda n: ConceptApplication(divides, Nat(2), n), computational_implementation=lambda n: n % 2 == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -146,7 +139,6 @@ def is_odd(): concept = Concept( name="is_odd", description="A number not divisible by 2", - symbolic_definition=lambda n: Not(ConceptApplication(divides, Nat(2), n)), computational_implementation=lambda n: n % 2 == 1, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -182,9 +174,6 @@ def proper_divisors_count(): concept = Concept( name="proper_divisors_count", description="Checks if k is the number of proper divisors of n", - symbolic_definition=lambda n, k: Equals( - k, SetCardinality(ConceptApplication(proper_divisors, n)) - ), computational_implementation=lambda n: len(proper_divisors.compute(n)), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -212,18 +201,6 @@ def tau_function_concept(): concept = Concept( name="tau", description="The number of divisors of n", - symbolic_definition=lambda n: SetCardinality( - Set( - domain=NatDomain(), - predicate=Lambda( - "d", - And( - ConceptApplication(divides, Var("d"), n), - ConceptApplication(less_than, Zero(), Var("d")), - ), - ), - ) - ), computational_implementation=lambda n: len( {i for i in range(1, n + 1) if n % i == 0}, ), @@ -247,9 +224,6 @@ def greater_than(): concept = Concept( name="greater_than", description="a > b if not (a ≤ b)", - symbolic_definition=lambda a, b: Exists( - "m", NatDomain(), Equals(b, addition(a, Var("m"))) - ), computational_implementation=lambda a, b: a > b, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -290,7 +264,6 @@ def zero_concept(): concept = Concept( name="zero", description="The number zero", - symbolic_definition=lambda: Nat(0), computational_implementation=lambda: 0, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -308,7 +281,6 @@ def one_concept(): concept = Concept( name="one", description="The number one", - symbolic_definition=lambda: Nat(1), computational_implementation=lambda: 1, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -326,7 +298,6 @@ def two_concept(): concept = Concept( name="two", description="The number two", - symbolic_definition=lambda: Nat(2), computational_implementation=lambda: 2, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -352,7 +323,6 @@ def three_concept(): concept = Concept( name="three", description="The number three", - symbolic_definition=lambda: Nat(3), computational_implementation=lambda: 3, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -370,7 +340,6 @@ def multi_output_function(): concept = Concept( name="multi_output", description="A function that returns multiple values", - symbolic_definition=lambda x: (x, x + 1), computational_implementation=lambda x: (x, x + 1), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -394,7 +363,6 @@ def successor_concept(): concept = Concept( name="successor", description="The successor function n -> n+1", - symbolic_definition=lambda n: Succ(n), computational_implementation=lambda n: n + 1, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -416,7 +384,6 @@ def multiply(): concept = Concept( name="multiply", description="Multiplication of two numbers", - symbolic_definition=lambda a, b: ConceptApplication(multiplication, a, b), computational_implementation=lambda a, b: a * b, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -458,11 +425,6 @@ def multiply3(): concept = Concept( name="multiply3", description="Multiplication of three numbers", - symbolic_definition=lambda a, b, c: ConceptApplication( - multiplication, - ConceptApplication(multiplication, a, b), - c, - ), computational_implementation=lambda a, b, c: a * b * c, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -499,7 +461,6 @@ def add2(): concept = Concept( name="add2", description="Add 2 to a number", - symbolic_definition=lambda x: ConceptApplication(addition, x, Nat(2)), computational_implementation=lambda x: x + 2, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -528,7 +489,6 @@ def add3(): concept = Concept( name="add3", description="Add 3 to a number", - symbolic_definition=lambda x: ConceptApplication(addition, x, Nat(3)), computational_implementation=lambda x: x + 3, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -558,7 +518,6 @@ def add_two_numbers(): concept = Concept( name="add_two_numbers", description="Addition of two numbers", - symbolic_definition=lambda a, b: ConceptApplication(addition, a, b), computational_implementation=lambda a, b: a + b, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -598,11 +557,6 @@ def add_three_numbers(): concept = Concept( name="add_three_numbers", description="Addition of three numbers", - symbolic_definition=lambda a, b, c: ConceptApplication( - addition, - ConceptApplication(addition, a, b), - c, - ), computational_implementation=lambda a, b, c: a + b + c, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -647,9 +601,6 @@ def many_args_concept(): concept = Concept( name="many_args", description="A function with many arguments", - symbolic_definition=lambda a, b, c, d, e, f, g, h: Set( - domain=NatDomain(), elements=[a, b, c, d, e, f, g, h] - ), computational_implementation=lambda a, b, c, d, e, f, g, h: { a, b, @@ -675,14 +626,6 @@ def mixed_types_concept(): concept = Concept( name="mixed_types", description="A function with mixed argument types", - symbolic_definition=lambda a, b, c: ConceptApplication( - ConceptApplication( - addition, - a, - ConceptApplication(SetCardinality, b), - ), - c, - ), computational_implementation=lambda a, b, c: a + len(b) + c, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -704,7 +647,6 @@ def equals_predicate(): concept = Concept( name="equals", description="Equality of two numbers", - symbolic_definition=lambda a, b: Equals(a, b), computational_implementation=lambda a, b: a == b, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -731,10 +673,6 @@ def set_of_divisors_concept(): concept = Concept( name="set_of_divisors", description="Returns the set of divisors of a number", - symbolic_definition=lambda n: Set( - domain=NatDomain(), - predicate=Lambda("x", ConceptApplication(divides, Var("x"), n)), - ), computational_implementation=lambda n: { i for i in range(1, n + 1) if n % i == 0 }, @@ -763,9 +701,6 @@ def divides_predicate(): concept = Concept( name="divides", description="Checks if one number divides another", - symbolic_definition=lambda a, b: Equals( - ConceptApplication(divides, a, b), - ), computational_implementation=lambda a, b: b % a == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -791,25 +726,6 @@ def prime_of_form_n2_plus_n_plus_1_predicate(): concept = Concept( name="is_prime_of_form_n2_plus_n_plus_1", description="Checks if a number is prime and of the form n^2 + n + 1", - symbolic_definition=lambda p: Exists( - "n", - NatDomain(), - And( - ConceptApplication(is_prime, p), - Equals( - ConceptApplication( - addition, - ConceptApplication( - addition, - ConceptApplication(multiplication, Var("n"), Var("n")), - Var("n"), - ), - Nat(1), - ), - p, - ), - ), - ), computational_implementation=lambda p: p > 1 and all(p % i != 0 for i in range(2, int(p**0.5) + 1)) and any(p == n**2 + n + 1 for n in range(int(p**0.5) + 1)), @@ -838,12 +754,6 @@ def multi_arg_predicate(): concept = Concept( name="sum_equals_product", description="Checks if a + b + c = a * b * c", - symbolic_definition=lambda a, b, c: Equals( - ConceptApplication(addition, ConceptApplication(addition, a, b), c), - ConceptApplication( - multiplication, ConceptApplication(multiplication, a, b), c - ), - ), computational_implementation=lambda a, b, c: a + b + c == a * b * c, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -874,9 +784,6 @@ def divides_and_even(): concept = Concept( name="divides_and_even", description="Tests if b divides a and b is even", - symbolic_definition=lambda a, b: And( - ConceptApplication(divides, b, a), ConceptApplication(is_even, b) - ), computational_implementation=lambda a, b: b != 0 and a % b == 0 and b % 2 == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -912,10 +819,6 @@ def add_multiply(): concept = Concept( name="add_multiply", description="Function that returns both sum and product of inputs", - symbolic_definition=lambda x, y: ( - ConceptApplication(addition, x, y), - ConceptApplication(multiplication, x, y), - ), computational_implementation=lambda x, y: (x + y, x * y), example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -943,10 +846,6 @@ def is_proper_divisor(): concept = Concept( name="is_proper_divisor", description="Tests if d is a proper divisor of n (d divides n and d != n)", - symbolic_definition=lambda n, d: And( - ConceptApplication(divides, d, n), - ConceptApplication(less_than, d, n), - ), computational_implementation=lambda n, d: n != d and n % d == 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, @@ -983,10 +882,6 @@ def divisor_mod_k_equals_r(): concept = Concept( name="divisor_mod_k_equals_r", description="Tests if d divides n and d % k == r", - symbolic_definition=lambda n, d, k, r: And( - ConceptApplication(divides, d, n), - Equals(ConceptApplication(lambda x, y: x % y, d, k), r), - ), computational_implementation=lambda n, d, k, r: ( d != 0 and n % d == 0 and d % k == r ), @@ -1035,9 +930,6 @@ def commutes(): concept = Concept( name="commutes", description="Tests if two elements commute under group operation", - symbolic_definition=lambda G, a, b: Equals( - Apply(G.op, a, b), Apply(G.op, b, a) - ), computational_implementation=lambda G, a, b: G.op(a, b) == G.op(b, a), example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, diff --git a/tests/productions/test_compose.py b/tests/productions/test_compose.py index 9a85288..cdf5daf 100644 --- a/tests/productions/test_compose.py +++ b/tests/productions/test_compose.py @@ -375,7 +375,6 @@ def test_empty_examples(self, compose_rule): empty_func = Concept( name="empty_func", description="Function with no examples", - symbolic_definition=lambda x: x + 1, computational_implementation=lambda x: x + 1, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -387,7 +386,6 @@ def test_empty_examples(self, compose_rule): empty_pred = Concept( name="empty_pred", description="Predicate with no examples", - symbolic_definition=lambda x: x > 0, computational_implementation=lambda x: x > 0, example_structure=ExampleStructure( concept_type=ConceptType.PREDICATE, diff --git a/tests/productions/test_map_iterate.py b/tests/productions/test_map_iterate.py index 6c7354c..90c4d09 100644 --- a/tests/productions/test_map_iterate.py +++ b/tests/productions/test_map_iterate.py @@ -309,9 +309,6 @@ def test_successor_to_addition(self, map_iterate_rule, successor_concept): for b in range(5): assert addition.compute(a, b) == a + b - # Check symbolic definition - assert "Fold" in str(addition.symbolic(Nat(3), Nat(4))) - def test_addition_to_multiplication( self, map_iterate_rule, add_two_numbers, zero_concept ): @@ -323,9 +320,6 @@ def test_addition_to_multiplication( for b in range(5): assert multiplication.compute(a, b) == a * b - # Check symbolic definition - assert "Fold" in str(multiplication.symbolic(Nat(3), Nat(4))) - def test_multiplication_to_power(self, map_iterate_rule, multiply, one_concept): """Test iterating multiplication to produce power.""" power = map_iterate_rule.apply(multiply, one_concept) @@ -338,9 +332,6 @@ def test_multiplication_to_power(self, map_iterate_rule, multiply, one_concept): else: assert power.compute(a, b) == a**b - # Check symbolic definition - assert "Fold" in str(power.symbolic(Nat(3), Nat(4))) - def test_nested_iteration( self, map_iterate_rule, diff --git a/tests/productions/test_match.py b/tests/productions/test_match.py index 9019b59..4853030 100644 --- a/tests/productions/test_match.py +++ b/tests/productions/test_match.py @@ -74,7 +74,6 @@ def test_invalid_parameterizations(self, match_rule, multiply): single_arg = Concept( name="single_arg", description="A function with a single argument", - symbolic_definition=lambda a: ConceptApplication(multiply, a, a), computational_implementation=lambda a: a * a, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -216,7 +215,6 @@ def test_invalid_concept_types(self, match_rule): dummy = Concept( name="dummy", description="A dummy concept", - symbolic_definition=lambda a: a, computational_implementation=lambda a: a, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -261,7 +259,6 @@ def test_insufficient_arity(self, match_rule): single_arg = Concept( name="single_arg", description="A function with a single argument", - symbolic_definition=lambda a: ConceptApplication(single_arg, a), computational_implementation=lambda a: a * 2, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -314,9 +311,6 @@ def test_nested_matching(self, match_rule, multiply3): square_times_plus = Concept( name="square_times_plus", description="Square of first argument times second argument plus third argument", - symbolic_definition=lambda a, b, c: ConceptApplication( - square_times_plus, a, b, c - ), computational_implementation=lambda a, b, c: (a * a * b) + c, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, diff --git a/tests/productions/test_negate.py b/tests/productions/test_negate.py index 955d7b5..c577b25 100644 --- a/tests/productions/test_negate.py +++ b/tests/productions/test_negate.py @@ -140,7 +140,6 @@ def test_invalid_input_type(self, negate_rule): conjecture = Conjecture( name="test_conjecture", description="A test conjecture", - symbolic_definition=lambda: True, example_structure=None, ) assert not negate_rule.can_apply( diff --git a/tests/productions/test_size.py b/tests/productions/test_size.py index 696404d..65f3b23 100644 --- a/tests/productions/test_size.py +++ b/tests/productions/test_size.py @@ -115,9 +115,6 @@ def test_invalid_parameterizations(self, size_rule): invalid_concept = Concept( name="invalid", description="A function that doesn't return a set", - symbolic_definition=lambda x: ConceptApplication( - addition, Var("x"), Nat(1) - ), computational_implementation=lambda x: x + 1, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -216,9 +213,6 @@ def test_invalid_concept_types(self, size_rule): invalid_concept = Concept( name="invalid", description="A function that doesn't return a set", - symbolic_definition=lambda x: ConceptApplication( - addition, Var("x"), Nat(1) - ), computational_implementation=lambda x: x + 1, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, diff --git a/tests/productions/test_specialize.py b/tests/productions/test_specialize.py index 833a336..868818a 100644 --- a/tests/productions/test_specialize.py +++ b/tests/productions/test_specialize.py @@ -56,7 +56,6 @@ def complex_specialized_concept(specialize_rule, successor_concept, zero_concept size_concept = Concept( name="size_of_(exists_(successor_indices_[0])_indices_[0])", description="Size of the set defined by existential quantification over successor", - symbolic_definition=lambda: SetCardinality(exists_expr), computational_implementation=lambda: float( "inf" ), # This set is infinite in size @@ -176,7 +175,6 @@ def test_specialize_binary_predicate_first_arg( five_concept = Concept( name="five", description="The number five", - symbolic_definition=lambda: Nat(5), computational_implementation=lambda: 5, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -250,7 +248,6 @@ def test_specialize_square_output(self, specialize_rule, square): four_concept = Concept( name="four", description="The number four", - symbolic_definition=lambda: Nat(4), computational_implementation=lambda: 4, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -403,7 +400,6 @@ def test_type_mismatch(self, specialize_rule, proper_divisors_count): string_concept = Concept( name="hello", description="The string 'hello'", - symbolic_definition=lambda: "hello", computational_implementation=lambda: "hello", example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -505,7 +501,6 @@ def test_invalid_parameterizations(self, specialize_rule, add2, one_concept, two string_concept = Concept( name="hello", description="The string 'hello'", - symbolic_definition=lambda: "hello", computational_implementation=lambda: "hello", example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -569,7 +564,6 @@ def test_nested_specialization( six_concept = Concept( name="six", description="The number six", - symbolic_definition=lambda: Nat(6), computational_implementation=lambda: 6, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, diff --git a/tests/test_knowledge_graph.py b/tests/test_knowledge_graph.py index 47a1826..f065b7c 100644 --- a/tests/test_knowledge_graph.py +++ b/tests/test_knowledge_graph.py @@ -199,7 +199,6 @@ def test_knowledge_graph_construction(): two_concept = Concept( name="two", description="The constant two", - symbolic_definition=lambda: Nat(2), computational_implementation=lambda: 2, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -213,7 +212,6 @@ def test_knowledge_graph_construction(): four_concept = Concept( name="four", description="The constant four", - symbolic_definition=lambda: Nat(4), computational_implementation=lambda: 4, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, diff --git a/tests/test_math_env_nat.py b/tests/test_math_env_nat.py index cd533af..20c0ebc 100644 --- a/tests/test_math_env_nat.py +++ b/tests/test_math_env_nat.py @@ -298,7 +298,6 @@ def test_math_env_nat_sequence(initial_graph, production_rules): two_concept = Concept( name="two", description="The natural number 2", - symbolic_definition=lambda: 2, computational_implementation=lambda: 2, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, @@ -360,7 +359,6 @@ def test_math_env_nat_sequence(initial_graph, production_rules): four_concept = Concept( name="four", description="The constant four", - symbolic_definition=lambda: Nat(4), computational_implementation=lambda: 4, example_structure=ExampleStructure( concept_type=ConceptType.FUNCTION, @@ -1120,7 +1118,6 @@ def test_entity_removal_with_dependencies(initial_graph, production_rules): two_concept = Concept( name="two", description="The natural number 2", - symbolic_definition=lambda: 2, computational_implementation=lambda: 2, example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT,