diff --git a/frame/configs/theory_building/initial_state/finite_field_basic.yaml b/frame/configs/theory_building/initial_state/finite_field_basic.yaml new file mode 100644 index 0000000..91f2d0c --- /dev/null +++ b/frame/configs/theory_building/initial_state/finite_field_basic.yaml @@ -0,0 +1,14 @@ +# Initial state: Basic Finite Field Concepts + +_target_: frame.knowledge_base.knowledge_graph.KnowledgeGraph +name: "finite_field_basic_initial" +description: "Initial knowledge graph with basic finite field concepts" + +# Import settings +import_from: "frame.knowledge_base.initial_concepts" +concepts: + - "create_finite_field_zero_concept" + - "create_finite_field_one_concept" + - "create_finite_field_addition_concept" + - "create_finite_field_multiplication_concept" + - "create_finite_field_equality_concept" \ No newline at end of file diff --git a/frame/environments/FF/calculations.py b/frame/environments/FF/calculations.py new file mode 100644 index 0000000..79f5d24 --- /dev/null +++ b/frame/environments/FF/calculations.py @@ -0,0 +1,97 @@ +from typing import Dict +from frame.environments.ground_truth_types import GroundTruthEntity, EntityType +from frame.knowledge_base.entities import FiniteFieldElement +from frame.tools.z3_template import Z3Template +import galois + +DEFAULT_FIELD = galois.GF(27) + +def get_order(a: FiniteFieldElement) -> int: + """Computes the multiplicative order of a finite field element.""" + if a.value == 0: + return 1 # By convention for this context + if a.value == 1: + return 1 + + # The galois library stores elements as numpy arrays, so we extract the int + element_val = int(a.value) + one_val = int(DEFAULT_FIELD(1)) + + count = 1 + val = element_val + while val != one_val: + val = (val * element_val) % DEFAULT_FIELD.order + count += 1 + return count + +FF_CALCULATIONS: Dict[str, GroundTruthEntity] = { + # TODO: Add discovered_names for these concepts + "ff_power": GroundTruthEntity( + canonical_name="ff_power", + entity_type=EntityType.CONCEPT, + description="Exponentiation of finite field elements", + computational_implementation=lambda a, n: a ** n, + ), + "ff_subtract": GroundTruthEntity( + canonical_name="ff_subtract", + entity_type=EntityType.CONCEPT, + description="Subtraction of finite field elements", + computational_implementation=lambda a, b: a - b, + ), + "ff_inverse": GroundTruthEntity( + canonical_name="ff_inverse", + entity_type=EntityType.CONCEPT, + description="Multiplicative inverse of a finite field element", + computational_implementation=lambda a: a.inverse() if int(a.value) != 0 else FiniteFieldElement(0), + ), + "ff_frobenius_map": GroundTruthEntity( + canonical_name="ff_frobenius_map", + entity_type=EntityType.CONCEPT, + description="The Frobenius automorphism x -> x^3", + computational_implementation=lambda a: a ** 3, + ), + "ff_element_order": GroundTruthEntity( + canonical_name="ff_element_order", + entity_type=EntityType.CONCEPT, + description="The multiplicative order of a finite field element", + computational_implementation=get_order, + ), +} + +FF_PREDICATE_CALCULATIONS: Dict[str, GroundTruthEntity] = { + # TODO: Add discovered_names for these concepts + "ff_is_primitive_element": GroundTruthEntity( + canonical_name="ff_is_primitive_element", + entity_type=EntityType.CONCEPT, + description="True if the element is a generator of the multiplicative group", + computational_implementation=lambda a: get_order(a) == (DEFAULT_FIELD.order - 1) if int(a.value) != 0 else False, + ), + "ff_is_square": GroundTruthEntity( + canonical_name="ff_is_square", + entity_type=EntityType.CONCEPT, + description="True if the element is a square", + computational_implementation=lambda a: a.is_square(), + ), + "ff_is_cube": GroundTruthEntity( + canonical_name="ff_is_cube", + entity_type=EntityType.CONCEPT, + description="True if the element is a cube", + computational_implementation=lambda a: a in {e*e*e for e in DEFAULT_FIELD.elements}, + ), +} + +FF_CONSTANTS_CALCULATIONS: Dict[str, GroundTruthEntity] = { + # TODO: Add discovered_names for these concepts + "ff_num_squares": GroundTruthEntity( + canonical_name="ff_num_squares", + entity_type=EntityType.CONCEPT, + description="The number of distinct squares in the finite field", + computational_implementation=lambda: len({e*e for e in DEFAULT_FIELD.elements}), + ), + "ff_num_cubes": GroundTruthEntity( + canonical_name="ff_num_cubes", + entity_type=EntityType.CONCEPT, + description="The number of distinct cubes in the finite field", + computational_implementation=lambda: len({e*e*e for e in DEFAULT_FIELD.elements}), + ), +} \ No newline at end of file diff --git a/frame/environments/FF/conjectures.py b/frame/environments/FF/conjectures.py new file mode 100644 index 0000000..76e408a --- /dev/null +++ b/frame/environments/FF/conjectures.py @@ -0,0 +1,51 @@ +from typing import Dict +from frame.environments.ground_truth_types import GroundTruthEntity, EntityType + +FF_CONJECTURES: Dict[str, GroundTruthEntity] = { + # TODO: Add discovered_names for these concepts + "ff_add_commutative": GroundTruthEntity( + canonical_name="ff_add_commutative", + entity_type=EntityType.CONJECTURE, + description="Addition is commutative in a finite field: a + b = b + a", + ), + "ff_multiply_commutative": GroundTruthEntity( + canonical_name="ff_multiply_commutative", + entity_type=EntityType.CONJECTURE, + description="Multiplication is commutative in a finite field: a * b = b * a", + ), + "ff_frobenius_identity": GroundTruthEntity( + canonical_name="ff_frobenius_identity", + entity_type=EntityType.CONJECTURE, + description="Frobenius identity for F_27: x^27 = x", + ), + "ff_multiplicative_group_cyclic": GroundTruthEntity( + canonical_name="ff_multiplicative_group_cyclic", + entity_type=EntityType.CONJECTURE, + description="The multiplicative group of a finite field is cyclic", + ), + "ff_additive_group_cyclic": GroundTruthEntity( + canonical_name="ff_additive_group_cyclic", + entity_type=EntityType.CONJECTURE, + description="The additive group of a finite field is cyclic", + ), + "ff_element_order_divides_group_order": GroundTruthEntity( + canonical_name="ff_element_order_divides_group_order", + entity_type=EntityType.CONJECTURE, + description="The order of an element divides the order of the multiplicative group", + ), + "ff_characteristic_p": GroundTruthEntity( + canonical_name="ff_characteristic_p", + entity_type=EntityType.CONJECTURE, + description="The characteristic of the field is p, so n*x = 0 for all x", + ), + "ff_cap_set_placeholder": GroundTruthEntity( + canonical_name="ff_cap_set_placeholder", + entity_type=EntityType.CONJECTURE, + description="Placeholder for the cap set problem/conjecture", + ), + "ff_symmetries": GroundTruthEntity( + canonical_name="ff_symmetries", + entity_type=EntityType.CONJECTURE, + description="Symmetries of the form c1 * x = c2 * x", + ), +} \ No newline at end of file diff --git a/frame/environments/FF/operations.py b/frame/environments/FF/operations.py new file mode 100644 index 0000000..bc90c70 --- /dev/null +++ b/frame/environments/FF/operations.py @@ -0,0 +1,78 @@ +from typing import Dict +from frame.environments.ground_truth_types import GroundTruthEntity, EntityType +from frame.knowledge_base.entities import FiniteFieldElement +from frame.tools.z3_template import Z3Template + +FF_FUNCTIONS: Dict[str, GroundTruthEntity] = { + "ff_add": GroundTruthEntity( + canonical_name="ff_add", + entity_type=EntityType.CONCEPT, + description="Addition of finite field elements", + computational_implementation=lambda a, b: a + b, + z3_translation=lambda a, b: Z3Template(f""" + # TODO: Implement Z3 translation for finite field addition + params 2; + bounded params 0; + ReturnExpr x_0 + x_1; + ReturnPred None; + """, a, b) + ), + "ff_multiply": GroundTruthEntity( + canonical_name="ff_multiply", + entity_type=EntityType.CONCEPT, + description="Multiplication of finite field elements", + computational_implementation=lambda a, b: a * b, + z3_translation=lambda a, b: Z3Template(f""" + # TODO: Implement Z3 translation for finite field multiplication + params 2; + bounded params 0; + ReturnExpr x_0 * x_1; + ReturnPred None; + """, a, b) + ), +} + +FF_PREDICATES: Dict[str, GroundTruthEntity] = { + "ff_eq": GroundTruthEntity( + canonical_name="ff_eq", + entity_type=EntityType.CONCEPT, + description="Equality of finite field elements", + computational_implementation=lambda a, b: a == b, + z3_translation=lambda a, b: Z3Template(f""" + # TODO: Implement Z3 translation for finite field equality + params 2; + bounded params 0; + ReturnExpr None; + ReturnPred x_0 == x_1; + """, a, b) + ), +} + +FF_CONSTANTS: Dict[str, GroundTruthEntity] = { + "ff_zero": GroundTruthEntity( + canonical_name="ff_zero", + entity_type=EntityType.CONCEPT, + description="The zero element in the finite field", + computational_implementation=lambda: FiniteFieldElement(0), + z3_translation=lambda: Z3Template(f""" + # TODO: Implement Z3 translation for finite field zero + params 0; + bounded params 0; + ReturnExpr 0; + ReturnPred None; + """) + ), + "ff_one": GroundTruthEntity( + canonical_name="ff_one", + entity_type=EntityType.CONCEPT, + description="The one element in the finite field", + computational_implementation=lambda: FiniteFieldElement(1), + z3_translation=lambda: Z3Template(f""" + # TODO: Implement Z3 translation for finite field one + params 0; + bounded params 0; + ReturnExpr 1; + ReturnPred None; + """) + ), +} \ No newline at end of file diff --git a/frame/environments/ground_truth_entities.py b/frame/environments/ground_truth_entities.py index 1cc84e9..046ebc4 100644 --- a/frame/environments/ground_truth_entities.py +++ b/frame/environments/ground_truth_entities.py @@ -25,6 +25,9 @@ from frame.environments.NT.operations import NT_FUNCTIONS, NT_PREDICATES, NT_NUMBERS from frame.environments.NT.calculations import NT_CALCULATIONS, NT_PREDICATE_CALCULATIONS, NT_EQ_CALCULATIONS from frame.environments.NT.conjectures import NT_CONJECTURES, NT_PRED_ALWAYS_TRUE +from frame.environments.FF.operations import FF_FUNCTIONS, FF_PREDICATES, FF_CONSTANTS +from frame.environments.FF.calculations import FF_CALCULATIONS, FF_PREDICATE_CALCULATIONS, FF_CONSTANTS_CALCULATIONS +from frame.environments.FF.conjectures import FF_CONJECTURES # ANSI color codes COLORS = { @@ -171,15 +174,16 @@ def normalize_name(name: str) -> str: # Create mapping of discovered names to canonical names name_mapping = {} - for entity in GROUND_TRUTH_ENTITIES.values(): + # TODO: This needs to be coordinated later. For now, using all. + for entity in {**GROUND_TRUTH_ENTITIES_NT, **GROUND_TRUTH_ENTITIES_FF}.values(): for discovered_name in entity.discovered_names: name_mapping[discovered_name] = entity.canonical_name # Recursively substitute known names return substitute_concept_name(name, name_mapping) -# Dictionary mapping normalized names to ground truth entities -GROUND_TRUTH_ENTITIES: Dict[str, GroundTruthEntity] = { +# Dictionary mapping normalized names to ground truth entities for Number Theory +GROUND_TRUTH_ENTITIES_NT: Dict[str, GroundTruthEntity] = { **NT_FUNCTIONS, **NT_PREDICATES, **NT_NUMBERS, @@ -190,6 +194,24 @@ def normalize_name(name: str) -> str: **NT_PRED_ALWAYS_TRUE } +# Dictionary mapping normalized names to ground truth entities for Finite Fields +GROUND_TRUTH_ENTITIES_FF: Dict[str, GroundTruthEntity] = { + **FF_FUNCTIONS, + **FF_PREDICATES, + **FF_CONSTANTS, + **FF_CALCULATIONS, + **FF_PREDICATE_CALCULATIONS, + **FF_CONSTANTS_CALCULATIONS, + **FF_CONJECTURES, +} + +# TODO: This needs to be coordinated later. For now, using all. +GROUND_TRUTH_ENTITIES: Dict[str, GroundTruthEntity] = { + **GROUND_TRUTH_ENTITIES_NT, + **GROUND_TRUTH_ENTITIES_FF +} + + def get_ground_truth_entity(name: str) -> Optional[GroundTruthEntity]: """ Get the ground truth entity for a given name, if it exists. @@ -210,6 +232,7 @@ def get_ground_truth_entity(name: str) -> Optional[GroundTruthEntity]: The ground truth entity if found, None otherwise """ normalized_name = normalize_name(name) + # TODO: This needs to be coordinated later. For now, using all. return GROUND_TRUTH_ENTITIES.get(normalized_name) def is_ground_truth_entity(name: str) -> bool: diff --git a/frame/environments/ground_truth_types.py b/frame/environments/ground_truth_types.py index 8c3ccae..f0b228f 100644 --- a/frame/environments/ground_truth_types.py +++ b/frame/environments/ground_truth_types.py @@ -23,7 +23,7 @@ def __post_init__(self): if self.discovered_names is None: self.discovered_names = set() - +# TODO(tsoukalas): Remove this upon determining it is not needed def is_prime(n): result = len([d for d in range(1, n+1) if n % d == 0]) == 2 return result \ No newline at end of file diff --git a/frame/knowledge_base/entities.py b/frame/knowledge_base/entities.py index 073ea85..d8f76f1 100644 --- a/frame/knowledge_base/entities.py +++ b/frame/knowledge_base/entities.py @@ -532,9 +532,9 @@ def evaluate(self) -> int: return self.value -class FiniteFieldOfOrder27(Expression): +class FiniteField(Expression): """ - Finite field of order 27. + By default, finite field of order 27. The elements are: [ 0, 1, 2, α, @@ -545,20 +545,80 @@ class FiniteFieldOfOrder27(Expression): 2α^2 + 2, 2α^2 + α, 2α^2 + α + 1, 2α^2 + α + 2, 2α^2 + 2α, 2α^2 + 2α + 1, 2α^2 + 2α + 2] """ - def __init__(self): - self.field = galois.GF(27) + def __init__(self, order=27): + self.order = order + self.field = galois.GF(order) self.field.repr("poly") + def __eq__(self, other: object) -> bool: + if not isinstance(other, FiniteField): + return NotImplemented + return self.order == other.order -class ElementOfFiniteFieldOfOrder27(Expression): + def __hash__(self) -> int: + return hash(self.order) + + def to_lean4(self) -> str: + """Return a Lean 4 representation of the finite field type.""" + # This is a placeholder; a proper representation might involve a specific library. + return f"FiniteField {self.order}" + + def to_prolog(self) -> str: + """Return a Prolog representation of the finite field type.""" + return f"finite_field_{self.order}" + + def to_z3(self) -> str: + """Return a Z3 representation of the finite field type.""" + # This would typically be a custom sort in Z3. + return f"FiniteField{self.order}" + + +DEFAULT_FINITE_FIELD = FiniteField(27) + + +class FiniteFieldElement(Expression): """ Represents a finite field element. """ - def __init__(self, value: int, field: FiniteFieldOfOrder27): - assert 0 <= value < 27, f"Value {value} must be between 0 and 26" + def __init__(self, value: int, field: FiniteField = DEFAULT_FINITE_FIELD): + assert 0 <= value < field.order, f"Value {value} must be between 0 and {field.order - 1}" self.value = field.field(value) self.field = field + def __add__(self, other: "FiniteFieldElement") -> "FiniteFieldElement": + if not isinstance(other, FiniteFieldElement) or self.field != other.field: + raise TypeError("Addition is only supported between elements of the same finite field.") + result_val = self.value + other.value + return FiniteFieldElement(int(result_val), self.field) + + def __mul__(self, other: "FiniteFieldElement") -> "FiniteFieldElement": + if not isinstance(other, FiniteFieldElement) or self.field != other.field: + raise TypeError("Multiplication is only supported between elements of the same finite field.") + result_val = self.value * other.value + return FiniteFieldElement(int(result_val), self.field) + + def __eq__(self, other: object) -> bool: + if not isinstance(other, FiniteFieldElement): + return NotImplemented + return self.field == other.field and self.value == other.value + + def __hash__(self) -> int: + return hash((int(self.value), self.field)) + + def to_lean4(self) -> str: + return str(self.value) + + def to_prolog(self) -> str: + return str(self.value) + + # TODO(tsoukalas): See what this should actually be in SMT-LIB + def to_z3(self) -> str: + return str(self.value) + + def evaluate(self) -> int: + return self.value + + class NatDomain(Expression): """Represents the domain/type of natural numbers""" @@ -717,6 +777,9 @@ def evaluate(self) -> Optional[bool]: if isinstance(self.left, Nat) and isinstance(self.right, Nat): return self.left.evaluate() == self.right.evaluate() + if isinstance(self.left, FiniteFieldElement) and isinstance(self.right, FiniteFieldElement): + return self.left.evaluate() == self.right.evaluate() + # Handle explicit Set equality if ( isinstance(self.left, Set) @@ -1200,6 +1263,7 @@ class ExampleType(Enum): FUNCTION = "function" GROUPELEMENT = "group_element" CONSTANT = "constant" + FINITEFIELD = "finite_field" ANY = "ANY" @staticmethod @@ -1287,6 +1351,8 @@ def _validate_single_type(self, value: Any, example_type: ExampleType) -> bool: return isinstance(value, tuple) and len(value) == 1 elif example_type == ExampleType.GROUPELEMENT: return True + elif example_type == ExampleType.FINITEFIELD: + return isinstance(value, FiniteFieldElement) return False def __str__(self) -> str: @@ -1357,6 +1423,8 @@ def _single_size(self, value: Any, example_type: ExampleType) -> int: return len(value) elif example_type == ExampleType.GROUP: return len(value.carrier) + elif example_type == ExampleType.FINITEFIELD: + return int(value.value) return float("inf") # Functions don't have a well-defined size def __eq__(self, other: "Example") -> bool: diff --git a/frame/knowledge_base/initial_concepts.py b/frame/knowledge_base/initial_concepts.py index 586dd57..e96fbcb 100644 --- a/frame/knowledge_base/initial_concepts.py +++ b/frame/knowledge_base/initial_concepts.py @@ -6,7 +6,7 @@ from frame.knowledge_base.entities import ( Concept, ExampleStructure, ExampleType, ConceptType, Zero, Succ, Nat, Fold, Lambda, Var, Exists, NatDomain, Equals, - ConceptApplication + ConceptApplication, FiniteField, FiniteFieldElement ) from frame.tools.z3_template import Z3Template @@ -358,6 +358,196 @@ def create_equality_concept(): eq.add_nonexample((3, 5)) return eq +# ============================================================================= +# Finite Field Concepts +# ============================================================================= + +def create_finite_field_zero_concept(): + """Factory function to create the zero concept for finite fields.""" + zero = Concept( + name="ff_zero", + description="The constant zero in a finite field", + computational_implementation=lambda: FiniteFieldElement(0), + example_structure=ExampleStructure( + concept_type=ConceptType.CONSTANT, + component_types=(ExampleType.FINITEFIELD,), + input_arity=0, + ), + can_add_examples=True, + can_add_nonexamples=True, + z3_translation=lambda: Z3Template( + """ + # TODO: Implement Z3 translation for finite field zero + params 0; + bounded params 0; + ReturnExpr 0; + ReturnPred None; + """, + ) + ) + zero.add_example((FiniteFieldElement(0),)) + zero.add_nonexample((FiniteFieldElement(1),)) + return zero + +def create_finite_field_one_concept(): + """Factory function to create the one concept for finite fields.""" + one = Concept( + name="ff_one", + description="The constant one in a finite field", + computational_implementation=lambda: FiniteFieldElement(1), + example_structure=ExampleStructure( + concept_type=ConceptType.CONSTANT, + component_types=(ExampleType.FINITEFIELD,), + input_arity=0, + ), + can_add_examples=True, + can_add_nonexamples=True, + z3_translation=lambda: Z3Template( + """ + # TODO: Implement Z3 translation for finite field one + params 0; + bounded params 0; + ReturnExpr 1; + ReturnPred None; + """, + ) + ) + one.add_example((FiniteFieldElement(1),)) + one.add_nonexample((FiniteFieldElement(0),)) + return one + +def create_finite_field_addition_concept(): + """Factory function to create the addition concept for finite fields.""" + add = Concept( + name="ff_add", + description="Addition of finite field elements", + computational_implementation=lambda a, b: a + b, + example_structure=ExampleStructure( + concept_type=ConceptType.FUNCTION, + component_types=(ExampleType.FINITEFIELD, ExampleType.FINITEFIELD, ExampleType.FINITEFIELD), + input_arity=2, + ), + can_add_examples=True, + can_add_nonexamples=True, + z3_translation=lambda a, b: Z3Template( + """ + # TODO: Implement Z3 translation for finite field addition + params 2; + bounded params 0; + ReturnExpr x_0 + x_1; + ReturnPred None; + """, + a, b + ) + ) + # Add examples (identity, commutativity, small values) + zero = FiniteFieldElement(0) + for i in range(5): + elem = FiniteFieldElement(i) + add.add_example((elem, zero, elem)) + add.add_example((zero, elem, elem)) + + a = FiniteFieldElement(5) + b = FiniteFieldElement(10) + c = FiniteFieldElement(12) + d = FiniteFieldElement(15) + + add.add_example((a, b, a + b)) + add.add_example((b, a, b + a)) # a+b = b+a + add.add_example((c, d, c + d)) + + # Add non-examples + add.add_nonexample((a, b, a + b + FiniteFieldElement(1))) + add.add_nonexample((c, d, c * d)) + add.add_nonexample((FiniteFieldElement(2), FiniteFieldElement(3), FiniteFieldElement(6))) + return add + +def create_finite_field_multiplication_concept(): + """Factory function to create the multiplication concept for finite fields.""" + mult = Concept( + name="ff_multiply", + description="Multiplication of finite field elements", + computational_implementation=lambda a, b: a * b, + example_structure=ExampleStructure( + concept_type=ConceptType.FUNCTION, + component_types=(ExampleType.FINITEFIELD, ExampleType.FINITEFIELD, ExampleType.FINITEFIELD), + input_arity=2, + ), + can_add_examples=True, + can_add_nonexamples=True, + z3_translation=lambda a, b: Z3Template( + """ + # TODO: Implement Z3 translation for finite field multiplication + params 2; + bounded params 0; + ReturnExpr x_0 * x_1; + ReturnPred None; + """, + a, b + ) + ) + # Add examples (zero, identity, commutativity, small values) + zero = FiniteFieldElement(0) + one = FiniteFieldElement(1) + for i in range(5): + elem = FiniteFieldElement(i) + mult.add_example((elem, one, elem)) + mult.add_example((one, elem, elem)) + mult.add_example((elem, zero, zero)) + mult.add_example((zero, elem, zero)) + + a = FiniteFieldElement(5) + b = FiniteFieldElement(10) + c = FiniteFieldElement(4) + d = FiniteFieldElement(7) # 4*7 = 28 mod 27 = 1 + + mult.add_example((a, b, a * b)) + mult.add_example((b, a, a * b)) # a*b = b*a + mult.add_example((c, d, c * d)) + + # Add non-examples + mult.add_nonexample((a, b, a + b)) + mult.add_nonexample((c, d, FiniteFieldElement(26))) + mult.add_nonexample((FiniteFieldElement(2), FiniteFieldElement(3), FiniteFieldElement(5))) + return mult + +def create_finite_field_equality_concept(): + """Factory function to create the equality concept for finite fields.""" + eq = Concept( + name="ff_eq", + description="a equals b in a finite field", + computational_implementation=lambda a, b: a == b, + example_structure=ExampleStructure( + concept_type=ConceptType.PREDICATE, + component_types=(ExampleType.FINITEFIELD, ExampleType.FINITEFIELD), + input_arity=2, + ), + can_add_examples=True, + can_add_nonexamples=True, + z3_translation=lambda a, b: Z3Template( + """ + # TODO: Implement Z3 translation for finite field equality + params 2; + bounded params 0; + ReturnExpr None; + ReturnPred x_0 == x_1; + """, + a, b + ) + ) + # Add examples (reflexive) + for i in range(5): + elem = FiniteFieldElement(i) + eq.add_example((elem, elem)) + + # Add non-examples + for i in range(1, 5): + eq.add_nonexample((FiniteFieldElement(i), FiniteFieldElement(i + 5))) + eq.add_nonexample((FiniteFieldElement(i + 5), FiniteFieldElement(i))) + eq.add_nonexample((FiniteFieldElement(10), FiniteFieldElement(20))) + return eq + + # ============================================================================= # Instantiate concepts for easy import elsewhere (e.g., demonstrations.py) # ============================================================================= @@ -367,5 +557,10 @@ def create_equality_concept(): addition_concept = create_addition_concept() multiplication_concept = create_multiplication_concept() divides_concept = create_divides_concept() -leq_than_concept = create_leq_than_concept() -equality_concept = create_equality_concept() \ No newline at end of file +leq_than_concept = create_leq_than_concept() +equality_concept = create_equality_concept() +ff_zero_concept = create_finite_field_zero_concept() +ff_one_concept = create_finite_field_one_concept() +ff_addition_concept = create_finite_field_addition_concept() +ff_multiplication_concept = create_finite_field_multiplication_concept() +ff_equality_concept = create_finite_field_equality_concept() \ No newline at end of file diff --git a/frame/repl/commands/basic.py b/frame/repl/commands/basic.py index b5b6a2d..eee6b91 100644 --- a/frame/repl/commands/basic.py +++ b/frame/repl/commands/basic.py @@ -184,6 +184,34 @@ def get_completions(self, state: REPLContext, partial: str) -> List[str]: return ["knowledge_graph.png"] return [f for f in ["knowledge_graph.png"] if f.startswith(partial)] +# Note(tsoukalas): This may be slightly buggy, fix later +class DomainCommand(BaseCommand): + """Switch the mathematical domain for the environment. + + Usage: domain + + This will reset the environment with the initial concepts for the chosen domain. + """ + + VALID_DOMAINS = ["nt", "ff"] + + def execute(self, state: REPLContext, *args) -> CommandResult: + """Execute the domain command.""" + if len(args) != 1 or args[0] not in self.VALID_DOMAINS: + return CommandResult(False, "Usage: domain ") + + domain_name = args[0] + + # The actual environment reset is handled in the REPL core engine + # This command just needs to return a success message. + return CommandResult(True, f"Domain changed to '{domain_name}'. Environment has been reset.") + + def get_completions(self, state: REPLContext, partial: str) -> List[str]: + """Get completions for domain names.""" + if not partial: + return self.VALID_DOMAINS + return [d for d in self.VALID_DOMAINS if d.startswith(partial)] + class ExitCommand(BaseCommand): """Exit the REPL.""" diff --git a/frame/repl/core/engine.py b/frame/repl/core/engine.py index 1bc075f..55f5684 100644 --- a/frame/repl/core/engine.py +++ b/frame/repl/core/engine.py @@ -16,7 +16,9 @@ class MathREPLCore(EventEmitter): """Core logic for the mathematical discovery REPL.""" def __init__(self, initial_graph: Optional[KnowledgeGraph] = None, - production_rules: Optional[List[ProductionRule]] = None): + production_rules: Optional[List[ProductionRule]] = None, + # To start the REPL with the Number Theory domain by default, change "ff" to "nt" + domain: str = "ff"): """Initialize the REPL core with optional initial state.""" super().__init__() @@ -28,7 +30,7 @@ def __init__(self, initial_graph: Optional[KnowledgeGraph] = None, # Initialize environment self.env = MathEnv( - initial_graph=initial_graph or self._create_initial_graph(), + initial_graph=initial_graph or self._create_initial_graph(domain), production_rules=production_rules or self._get_default_rules(), max_steps=1000, enumerate_actions=True @@ -53,6 +55,14 @@ def execute_command(self, command_str: str) -> CommandResult: cmd_name, args = parts[0], parts[1:] + # Handle the domain command as a special case to reset the environment + if cmd_name == "domain": + if len(args) != 1 or args[0] not in ['nt', 'ff']: + return CommandResult(False, "Usage: domain ") + domain_name = args[0] + self.reset_with_domain(domain_name) + return CommandResult(True, f"Domain changed to '{domain_name}'. Environment has been reset.") + # Get command handler command = self.registry.get_command(cmd_name) if not command: @@ -117,21 +127,38 @@ def _check_for_new_entities(self, old_state: StateSnapshot, new_state: StateSnap conjecture, _, _ = new_state.graph.get_node(conjecture_id) self.emit(create_new_entity_event(conjecture, conjecture_id, "conjecture")) - def _create_initial_graph(self) -> KnowledgeGraph: - """Create initial graph with Zero and Successor.""" - from frame.knowledge_base.initial_concepts import create_successor_concept, zero_concept, create_equality_concept - - graph = KnowledgeGraph() - - # Add Zero and Successor concepts - zero = zero_concept - successor = create_successor_concept() - equals = create_equality_concept() - - zero_id = graph.add_concept(zero) - succ_id = graph.add_concept(successor) - equals_id = graph.add_concept(equals) + def reset_with_domain(self, domain_name: str): + """Resets the environment with a new initial graph for the given domain.""" + new_initial_graph = self._create_initial_graph(domain_name) + self.env.initial_graph = new_initial_graph + self.env.reset() + self.history.clear() + def _create_initial_graph(self, domain: str = "ff") -> KnowledgeGraph: + """Create initial graph based on the specified domain.""" + graph = KnowledgeGraph() + + if domain == "nt": + from frame.knowledge_base.initial_concepts import create_successor_concept, zero_concept, create_equality_concept + graph.add_concept(zero_concept) + graph.add_concept(create_successor_concept()) + graph.add_concept(create_equality_concept()) + elif domain == "ff": + from frame.knowledge_base.initial_concepts import ( + create_finite_field_zero_concept, + create_finite_field_one_concept, + create_finite_field_addition_concept, + create_finite_field_multiplication_concept, + create_finite_field_equality_concept, + ) + graph.add_concept(create_finite_field_zero_concept()) + graph.add_concept(create_finite_field_one_concept()) + graph.add_concept(create_finite_field_addition_concept()) + graph.add_concept(create_finite_field_multiplication_concept()) + graph.add_concept(create_finite_field_equality_concept()) + else: + raise ValueError(f"Unknown domain for initial graph: {domain}") + return graph def _get_default_rules(self) -> List[ProductionRule]: diff --git a/frame/repl/interface/cli.py b/frame/repl/interface/cli.py index e0456a1..77f4a9c 100644 --- a/frame/repl/interface/cli.py +++ b/frame/repl/interface/cli.py @@ -59,7 +59,7 @@ def __init__(self, initial_graph: Optional[KnowledgeGraph] = None): from frame.repl.commands.basic import ( HelpCommand, ListCommand, RenameCommand, ClearCommand, VisualizeCommand, ExitCommand, - SaveCommand, RemoveCommand + SaveCommand, RemoveCommand, DomainCommand ) from frame.repl.commands.math import ApplyRuleCommand, InspectCommand, ComputeCommand @@ -74,6 +74,7 @@ def __init__(self, initial_graph: Optional[KnowledgeGraph] = None): self.repl.registry.register(SaveCommand()) self.repl.registry.register(ComputeCommand()) self.repl.registry.register(RemoveCommand()) + self.repl.registry.register(DomainCommand()) # Cache commonly used commands self._inspect_cmd = self.repl.registry.get_command('inspect')