diff --git a/frame/configs/ff_generate_interestingness_funsearch.yaml b/frame/configs/ff_generate_interestingness_funsearch.yaml index 8db82dc..b8a6fae 100644 --- a/frame/configs/ff_generate_interestingness_funsearch.yaml +++ b/frame/configs/ff_generate_interestingness_funsearch.yaml @@ -30,11 +30,13 @@ initial_state: concepts: - "create_finite_field_zero_concept" - "create_finite_field_one_concept" - - "create_finite_field_three_concept" - - "create_finite_field_nine_concept" + - "create_finite_field_alpha_concept" + - "create_finite_field_alpha_squared_concept" - "create_finite_field_addition_concept" - "create_finite_field_multiplication_concept" - - "create_finite_field_equality_concept" + - "create_finite_field_equality_concept" + - "create_finite_field_additive_inverse_concept" + - "create_finite_field_multiplicative_inverse_concept" # Experiment settings override experiment: diff --git a/frame/configs/theory_building/initial_state/finite_field_basic.yaml b/frame/configs/theory_building/initial_state/finite_field_basic.yaml index e1f1fcf..992431a 100644 --- a/frame/configs/theory_building/initial_state/finite_field_basic.yaml +++ b/frame/configs/theory_building/initial_state/finite_field_basic.yaml @@ -9,8 +9,10 @@ import_from: "frame.knowledge_base.initial_concepts" concepts: - "create_finite_field_zero_concept" - "create_finite_field_one_concept" - - "create_finite_field_three_concept" - - "create_finite_field_nine_concept" + - "create_finite_field_alpha_concept" + - "create_finite_field_alpha_squared_concept" - "create_finite_field_addition_concept" - "create_finite_field_multiplication_concept" - - "create_finite_field_equality_concept" \ No newline at end of file + - "create_finite_field_equality_concept" + - "create_finite_field_additive_inverse_concept" + - "create_finite_field_multiplicative_inverse_concept" \ No newline at end of file diff --git a/frame/environments/FF/calculations.py b/frame/environments/FF/calculations.py index 79f5d24..96b3960 100644 --- a/frame/environments/FF/calculations.py +++ b/frame/environments/FF/calculations.py @@ -1,60 +1,84 @@ from typing import Dict from frame.environments.ground_truth_types import GroundTruthEntity, EntityType -from frame.knowledge_base.entities import FiniteFieldElement +from frame.knowledge_base.entities import FiniteFieldElement, DEFAULT_FINITE_FIELD 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_add_zero": GroundTruthEntity( + canonical_name="ff_add_zero", + entity_type=EntityType.CONCEPT, + description="Addition of finite field element with zero", + computational_implementation=lambda a: a + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)), + z3_translation=lambda a: Z3Template(f"", a), + discovered_names={"specialized_(ff_add_at_0_to_ff_zero)", "specialized_(ff_add_at_1_to_ff_zero)" } + ), + "ff_add_one": GroundTruthEntity( + canonical_name="ff_add_one", + entity_type=EntityType.CONCEPT, + description="Addition of finite field element with one", + computational_implementation=lambda a: a + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)), + z3_translation=lambda a: Z3Template(f"", a), + discovered_names={"specialized_(ff_add_at_0_to_ff_one)", "specialized_(ff_add_at_1_to_ff_one)" } + ), + "ff_add_alpha": GroundTruthEntity( + canonical_name="ff_add_alpha", + entity_type=EntityType.CONCEPT, + description="Addition of finite field element with alpha", + computational_implementation=lambda a: a + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(3)), + z3_translation=lambda a: Z3Template(f"", a), + discovered_names={"specialized_(ff_add_at_0_to_ff_alpha)", "specialized_(ff_add_at_1_to_ff_alpha)" } + ), + "ff_add_alpha_squared": GroundTruthEntity( + canonical_name="ff_add_alpha_squared", + entity_type=EntityType.CONCEPT, + description="Addition of finite field element with alpha squared", + computational_implementation=lambda a: a + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(9)), + z3_translation=lambda a: Z3Template(f"", a), + discovered_names={"specialized_(ff_add_at_0_to_ff_alpha_squared)", "specialized_(ff_add_at_1_to_ff_alpha_squared)" } + ), "ff_power": GroundTruthEntity( canonical_name="ff_power", entity_type=EntityType.CONCEPT, description="Exponentiation of finite field elements", computational_implementation=lambda a, n: a ** n, + discovered_names={"iterate_(ff_multiply_with_ff_one)"}, ), "ff_subtract": GroundTruthEntity( canonical_name="ff_subtract", entity_type=EntityType.CONCEPT, description="Subtraction of finite field elements", + discovered_names={"compose_(ff_additive_inverse_with_ff_add_output_to_input_map={0: 1})"}, computational_implementation=lambda a, b: a - b, ), - "ff_inverse": GroundTruthEntity( - canonical_name="ff_inverse", + "ff_division": GroundTruthEntity( + canonical_name="ff_division", + entity_type=EntityType.CONCEPT, + description="Division of finite field elements", + discovered_names={"compose_(ff_multiplicative_inverse_with_ff_multiply_output_to_input_map={0: 1})"}, + computational_implementation=lambda a, b: a / b, + ), + "ff_square": GroundTruthEntity( + canonical_name="ff_square", 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), + description="Square of a finite field element", + computational_implementation=lambda a: a * a, + discovered_names={"matched_(ff_multiply_indices_[0, 1])", "specialized_(ff_power_at_1_to_two)"} ), "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, + discovered_names={"specialized_(ff_power_at_1_to_three)"} ), "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, + computational_implementation=lambda a: DEFAULT_FINITE_FIELD.multiplicative_order(a.value), ), } @@ -64,19 +88,21 @@ def get_order(a: FiniteFieldElement) -> int: 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, + computational_implementation=lambda a: DEFAULT_FINITE_FIELD.multiplicative_order(a.value) == DEFAULT_FINITE_FIELD.order - 1, ), "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(), + computational_implementation=lambda a: DEFAULT_FINITE_FIELD.is_square(a.value), + discovered_names={"exists_(ff_square_indices_[0])"} ), "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}, + computational_implementation=lambda a: a in {e*e*e for e in DEFAULT_FINITE_FIELD.elements}, + discovered_names={"exists_(ff_frobenius_map_indices_[0])"} ), } diff --git a/frame/environments/FF/operations.py b/frame/environments/FF/operations.py index 87f6e56..4a160f0 100644 --- a/frame/environments/FF/operations.py +++ b/frame/environments/FF/operations.py @@ -1,6 +1,6 @@ from typing import Dict from frame.environments.ground_truth_types import GroundTruthEntity, EntityType -from frame.knowledge_base.entities import FiniteFieldElement +from frame.knowledge_base.entities import FiniteFieldElement, DEFAULT_FINITE_FIELD from frame.tools.z3_template import Z3Template FF_FUNCTIONS: Dict[str, GroundTruthEntity] = { @@ -9,26 +9,28 @@ 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) + z3_translation=lambda a, b: Z3Template(f"", 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) + z3_translation=lambda a, b: Z3Template(f"", a, b) + ), + "ff_additive_inverse": GroundTruthEntity( + canonical_name="ff_additive_inverse", + entity_type=EntityType.CONCEPT, + description="Additive inverse of a finite field element", + computational_implementation=lambda a: -a, + z3_translation=lambda a: Z3Template(f"", a) + ), + "ff_multiplicative_inverse": GroundTruthEntity( + canonical_name="ff_multiplicative_inverse", + entity_type=EntityType.CONCEPT, + description="Multiplicative inverse of a finite field element", + computational_implementation=lambda a: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)) / a, + z3_translation=lambda a: Z3Template(f"", a) ), } @@ -38,13 +40,7 @@ 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) + z3_translation=lambda a, b: Z3Template(f"", a, b) ), } @@ -53,52 +49,28 @@ 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; - """) + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)), + z3_translation=lambda: Z3Template(f"") ), "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; - """) + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)), + z3_translation=lambda: Z3Template(f"") ), - "ff_three": GroundTruthEntity( - canonical_name="ff_three", + "ff_alpha": GroundTruthEntity( + canonical_name="ff_alpha", entity_type=EntityType.CONCEPT, - description="The three element in the finite field", - computational_implementation=lambda: FiniteFieldElement(3), - z3_translation=lambda: Z3Template(f""" - # TODO: Implement Z3 translation for finite field three - params 0; - bounded params 0; - ReturnExpr 3; - ReturnPred None; - """) + description="The alpha element in the finite field", + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(3)), + z3_translation=lambda: Z3Template(f"") ), - "ff_nine": GroundTruthEntity( - canonical_name="ff_nine", + "ff_alpha_squared": GroundTruthEntity( + canonical_name="ff_alpha_squared", entity_type=EntityType.CONCEPT, - description="The nine element in the finite field", - computational_implementation=lambda: FiniteFieldElement(9), - z3_translation=lambda: Z3Template(f""" - # TODO: Implement Z3 translation for finite field nine - params 0; - bounded params 0; - ReturnExpr 9; - ReturnPred None; - """) + description="The alpha squared element in the finite field", + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(9)), + z3_translation=lambda: Z3Template(f"") ), } \ No newline at end of file diff --git a/frame/environments/FF/repl_commands.txt b/frame/environments/FF/repl_commands.txt new file mode 100644 index 0000000..504bfd7 --- /dev/null +++ b/frame/environments/FF/repl_commands.txt @@ -0,0 +1,50 @@ +apply iter successor +apply iter add zero +apply match add indices_to_match=[0,1] +apply match multiply indices_to_match=[0,1] +apply specialize successor zero index_to_specialize=0 +apply specialize successor one index_to_specialize=0 +apply specialize successor two index_to_specialize=0 +apply specialize successor three index_to_specialize=0 +apply specialize successor four index_to_specialize=0 +apply specialize successor five index_to_specialize=0 +apply specialize successor six index_to_specialize=0 +apply specialize successor seven index_to_specialize=0 +apply specialize successor eight index_to_specialize=0 +apply specialize successor nine index_to_specialize=0 +apply specialize successor ten index_to_specialize=0 +apply specialize successor eleven index_to_specialize=0 +apply specialize successor twelve index_to_specialize=0 +apply specialize successor thirteen index_to_specialize=0 +apply specialize successor fourteen index_to_specialize=0 +apply specialize successor fifteen index_to_specialize=0 +apply specialize successor sixteen index_to_specialize=0 +apply specialize successor seventeen index_to_specialize=0 +apply specialize successor eighteen index_to_specialize=0 +apply specialize successor nineteen index_to_specialize=0 +apply specialize successor twenty index_to_specialize=0 +apply specialize successor twenty_one index_to_specialize=0 +apply specialize successor twenty_two index_to_specialize=0 +apply specialize successor twenty_three index_to_specialize=0 +apply specialize successor twenty_four index_to_specialize=0 +apply specialize successor twenty_five index_to_specialize=0 +apply specialize successor twenty_six index_to_specialize=0 +apply iter multiply one + + +apply specialize ff_add ff_zero index_to_specialize=0 +apply specialize ff_add ff_one index_to_specialize=0 +apply specialize ff_add ff_alpha index_to_specialize=0 +apply specialize ff_add ff_alpha_squared index_to_specialize=0 +apply iter ff_multiply ff_one +apply compose ff_additive_inverse ff_add output_to_input_map={0:1} +apply compose ff_multiplicative_inverse ff_multiply output_to_input_map={0:1} +apply specialize ff_power two index_to_specialize=1 +apply specialize ff_power three index_to_specialize=1 +apply specialize ff_power twenty_seven index_to_specialize=1 +apply exists ff_square indices_to_quantify=[0] +apply exists ff_frobenius_map indices_to_quantify=[0] + + + + diff --git a/frame/environments/NT/operations.py b/frame/environments/NT/operations.py index 7a6fd95..11d20d1 100644 --- a/frame/environments/NT/operations.py +++ b/frame/environments/NT/operations.py @@ -413,7 +413,154 @@ description="The natural number 6", computational_implementation=lambda: 6, discovered_names={"specialized_(successor_at_0_to_five)"} - ), + ), + "seven": GroundTruthEntity( + canonical_name="seven", + entity_type=EntityType.CONCEPT, + description="The natural number 7", + computational_implementation=lambda: 7, + discovered_names={"specialized_(successor_at_0_to_six)"} + ), + "eight": GroundTruthEntity( + canonical_name="eight", + entity_type=EntityType.CONCEPT, + description="The natural number 8", + computational_implementation=lambda: 8, + discovered_names={"specialized_(successor_at_0_to_seven)"} + ), + "nine": GroundTruthEntity( + canonical_name="nine", + entity_type=EntityType.CONCEPT, + description="The natural number 9", + computational_implementation=lambda: 9, + discovered_names={"specialized_(successor_at_0_to_eight)"} + ), + "ten": GroundTruthEntity( + canonical_name="ten", + entity_type=EntityType.CONCEPT, + description="The natural number 10", + computational_implementation=lambda: 10, + discovered_names={"specialized_(successor_at_0_to_nine)"} + ), + "eleven": GroundTruthEntity( + canonical_name="eleven", + entity_type=EntityType.CONCEPT, + description="The natural number 11", + computational_implementation=lambda: 11, + discovered_names={"specialized_(successor_at_0_to_ten)"} + ), + "twelve": GroundTruthEntity( + canonical_name="twelve", + entity_type=EntityType.CONCEPT, + description="The natural number 12", + computational_implementation=lambda: 12, + discovered_names={"specialized_(successor_at_0_to_eleven)"} + ), + "thirteen": GroundTruthEntity( + canonical_name="thirteen", + entity_type=EntityType.CONCEPT, + description="The natural number 13", + computational_implementation=lambda: 13, + discovered_names={"specialized_(successor_at_0_to_twelve)"} + ), + "fourteen": GroundTruthEntity( + canonical_name="fourteen", + entity_type=EntityType.CONCEPT, + description="The natural number 14", + computational_implementation=lambda: 14, + discovered_names={"specialized_(successor_at_0_to_thirteen)"} + ), + "fifteen": GroundTruthEntity( + canonical_name="fifteen", + entity_type=EntityType.CONCEPT, + description="The natural number 15", + computational_implementation=lambda: 15, + discovered_names={"specialized_(successor_at_0_to_fourteen)"} + ), + "sixteen": GroundTruthEntity( + canonical_name="sixteen", + entity_type=EntityType.CONCEPT, + description="The natural number 16", + computational_implementation=lambda: 16, + discovered_names={"specialized_(successor_at_0_to_fifteen)"} + ), + "seventeen": GroundTruthEntity( + canonical_name="seventeen", + entity_type=EntityType.CONCEPT, + description="The natural number 17", + computational_implementation=lambda: 17, + discovered_names={"specialized_(successor_at_0_to_sixteen)"} + ), + "eighteen": GroundTruthEntity( + canonical_name="eighteen", + entity_type=EntityType.CONCEPT, + description="The natural number 18", + computational_implementation=lambda: 18, + discovered_names={"specialized_(successor_at_0_to_seventeen)"} + ), + "nineteen": GroundTruthEntity( + canonical_name="nineteen", + entity_type=EntityType.CONCEPT, + description="The natural number 19", + computational_implementation=lambda: 19, + discovered_names={"specialized_(successor_at_0_to_eighteen)"} + ), + "twenty": GroundTruthEntity( + canonical_name="twenty", + entity_type=EntityType.CONCEPT, + description="The natural number 20", + computational_implementation=lambda: 20, + discovered_names={"specialized_(successor_at_0_to_nineteen)"} + ), + "twenty_one": GroundTruthEntity( + canonical_name="twenty_one", + entity_type=EntityType.CONCEPT, + description="The natural number 21", + computational_implementation=lambda: 21, + discovered_names={"specialized_(successor_at_0_to_twenty)"} + ), + "twenty_two": GroundTruthEntity( + canonical_name="twenty_two", + entity_type=EntityType.CONCEPT, + description="The natural number 22", + computational_implementation=lambda: 22, + discovered_names={"specialized_(successor_at_0_to_twenty_one)"} + ), + "twenty_three": GroundTruthEntity( + canonical_name="twenty_three", + entity_type=EntityType.CONCEPT, + description="The natural number 23", + computational_implementation=lambda: 23, + discovered_names={"specialized_(successor_at_0_to_twenty_two)"} + ), + "twenty_four": GroundTruthEntity( + canonical_name="twenty_four", + entity_type=EntityType.CONCEPT, + description="The natural number 24", + computational_implementation=lambda: 24, + discovered_names={"specialized_(successor_at_0_to_twenty_three)"} + ), + "twenty_five": GroundTruthEntity( + canonical_name="twenty_five", + entity_type=EntityType.CONCEPT, + description="The natural number 25", + computational_implementation=lambda: 25, + discovered_names={"specialized_(successor_at_0_to_twenty_four)"} + ), + "twenty_six": GroundTruthEntity( + canonical_name="twenty_six", + entity_type=EntityType.CONCEPT, + description="The natural number 26", + computational_implementation=lambda: 26, + discovered_names={"specialized_(successor_at_0_to_twenty_five)"} + ), + "twenty_seven": GroundTruthEntity( + canonical_name="twenty_seven", + entity_type=EntityType.CONCEPT, + description="The natural number 27", + computational_implementation=lambda: 27, + discovered_names={"specialized_(successor_at_0_to_twenty_six)"} + ), "gt_five": GroundTruthEntity( canonical_name="gt_five", entity_type=EntityType.CONCEPT, diff --git a/frame/knowledge_base/entities.py b/frame/knowledge_base/entities.py index 865e683..d64941f 100644 --- a/frame/knowledge_base/entities.py +++ b/frame/knowledge_base/entities.py @@ -597,6 +597,25 @@ def __mul__(self, other: "FiniteFieldElement") -> "FiniteFieldElement": result_val = self.value * other.value return FiniteFieldElement(int(result_val), self.field) + def __truediv__(self, other: "FiniteFieldElement") -> "FiniteFieldElement": + if not isinstance(other, FiniteFieldElement) or self.field != other.field: + raise TypeError("Division is only supported between elements of the same finite field.") + result_val = self.value / other.value + return FiniteFieldElement(int(result_val), self.field) + + def __neg__(self) -> "FiniteFieldElement": + return FiniteFieldElement(int(-self.value), self.field) + + def __sub__(self, other: "FiniteFieldElement") -> "FiniteFieldElement": + if not isinstance(other, FiniteFieldElement) or self.field != other.field: + raise TypeError("Subtraction is only supported between elements of the same finite field.") + result_val = self.value - other.value + return FiniteFieldElement(int(result_val), self.field) + + def __pow__(self, other: int) -> "FiniteFieldElement": + result_val = self.value ** other + return FiniteFieldElement(int(result_val), self.field) + def __str__(self) -> str: return f"GF({self.field.order})({self.value})" diff --git a/frame/knowledge_base/initial_concepts.py b/frame/knowledge_base/initial_concepts.py index eb07558..57fdc6c 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, FiniteField, FiniteFieldElement + ConceptApplication, FiniteField, FiniteFieldElement, DEFAULT_FINITE_FIELD ) from frame.tools.z3_template import Z3Template @@ -367,7 +367,7 @@ def create_finite_field_zero_concept(): zero = Concept( name="ff_zero", description="The constant zero in a finite field", - computational_implementation=lambda: FiniteFieldElement(0), + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)), example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, component_types=(ExampleType.FINITEFIELD_ELEMENT,), @@ -394,7 +394,7 @@ def create_finite_field_one_concept(): one = Concept( name="ff_one", description="The constant one in a finite field", - computational_implementation=lambda: FiniteFieldElement(1), + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)), example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, component_types=(ExampleType.FINITEFIELD_ELEMENT,), @@ -416,12 +416,12 @@ def create_finite_field_one_concept(): one.add_nonexample((FiniteFieldElement(0),)) return one -def create_finite_field_three_concept(): - """Factory function to create the three concept for finite fields (a generator).""" - three = Concept( - name="ff_three", - description="The constant three in a finite field (a generator)", - computational_implementation=lambda: FiniteFieldElement(3), +def create_finite_field_alpha_concept(): + """Factory function to create the alpha concept for finite fields (a generator).""" + alpha = Concept( + name="ff_alpha", + description="The constant alpha in a finite field (a generator)", + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(3)), example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, component_types=(ExampleType.FINITEFIELD_ELEMENT,), @@ -429,27 +429,17 @@ def create_finite_field_three_concept(): ), can_add_examples=True, can_add_nonexamples=True, - z3_translation=lambda: Z3Template( - """ - # TODO: Implement Z3 translation for finite field three - params 0; - bounded params 0; - ReturnExpr 3; - ReturnPred None; - """, - ) + z3_translation=lambda: Z3Template("") ) - three.add_example((FiniteFieldElement(3),)) - three.add_nonexample((FiniteFieldElement(0),)) - three.add_nonexample((FiniteFieldElement(1),)) - return three - -def create_finite_field_nine_concept(): - """Factory function to create the nine concept for finite fields (a generator).""" - nine = Concept( - name="ff_nine", - description="The constant nine in a finite field (a generator)", - computational_implementation=lambda: FiniteFieldElement(9), + + return alpha + +def create_finite_field_alpha_squared_concept(): + """Factory function to create the alpha squared concept for finite fields (a generator).""" + alpha_squared = Concept( + name="ff_alpha_squared", + description="The constant alpha squared in a finite field (a generator)", + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(9)), example_structure=ExampleStructure( concept_type=ConceptType.CONSTANT, component_types=(ExampleType.FINITEFIELD_ELEMENT,), @@ -457,21 +447,10 @@ def create_finite_field_nine_concept(): ), can_add_examples=True, can_add_nonexamples=True, - z3_translation=lambda: Z3Template( - """ - # TODO: Implement Z3 translation for finite field nine - params 0; - bounded params 0; - ReturnExpr 9; - ReturnPred None; - """, - ) + z3_translation=lambda: Z3Template("") ) - nine.add_example((FiniteFieldElement(9),)) - nine.add_nonexample((FiniteFieldElement(0),)) - nine.add_nonexample((FiniteFieldElement(1),)) - nine.add_nonexample((FiniteFieldElement(3),)) - return nine + + return alpha_squared def create_finite_field_addition_concept(): """Factory function to create the addition concept for finite fields.""" @@ -498,25 +477,25 @@ def create_finite_field_addition_concept(): ) ) # Add examples (identity, commutativity, small values) - zero = FiniteFieldElement(0) + zero = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)) for i in range(5): - elem = FiniteFieldElement(i) + elem = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(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) + a = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(5)) + b = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(10)) + c = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(12)) + d = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(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((a, b, a + b + FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)))) add.add_nonexample((c, d, c * d)) - add.add_nonexample((FiniteFieldElement(2), FiniteFieldElement(3), FiniteFieldElement(6))) + add.add_nonexample((FiniteFieldElement(DEFAULT_FINITE_FIELD.field(2)), FiniteFieldElement(DEFAULT_FINITE_FIELD.field(3)), FiniteFieldElement(DEFAULT_FINITE_FIELD.field(6)))) return add def create_finite_field_multiplication_concept(): @@ -544,19 +523,19 @@ def create_finite_field_multiplication_concept(): ) ) # Add examples (zero, identity, commutativity, small values) - zero = FiniteFieldElement(0) - one = FiniteFieldElement(1) + zero = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)) + one = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)) for i in range(5): - elem = FiniteFieldElement(i) + elem = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(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 + a = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(5)) + b = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(10)) + c = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(4)) + d = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(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 @@ -564,10 +543,44 @@ def create_finite_field_multiplication_concept(): # 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))) + mult.add_nonexample((c, d, FiniteFieldElement(DEFAULT_FINITE_FIELD.field(26)))) + mult.add_nonexample((FiniteFieldElement(DEFAULT_FINITE_FIELD.field(2)), FiniteFieldElement(DEFAULT_FINITE_FIELD.field(3)), FiniteFieldElement(DEFAULT_FINITE_FIELD.field(5)))) return mult +def create_finite_field_additive_inverse_concept(): + """Factory function to create the additive inverse concept for finite fields.""" + add_inv = Concept( + name="ff_additive_inverse", + description="Additive inverse of a finite field element", + computational_implementation=lambda a: -a, + example_structure=ExampleStructure( + concept_type=ConceptType.FUNCTION, + component_types=(ExampleType.FINITEFIELD_ELEMENT, ExampleType.FINITEFIELD_ELEMENT), + input_arity=1, + ), + can_add_examples=True, + can_add_nonexamples=True, + z3_translation=lambda a: Z3Template("") + ) + return add_inv + +def create_finite_field_multiplicative_inverse_concept(): + """Factory function to create the multiplicative inverse concept for finite fields.""" + mult_inv = Concept( + name="ff_multiplicative_inverse", + description="Multiplicative inverse of a finite field element", + computational_implementation=lambda a: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)) / a, + example_structure=ExampleStructure( + concept_type=ConceptType.FUNCTION, + component_types=(ExampleType.FINITEFIELD_ELEMENT, ExampleType.FINITEFIELD_ELEMENT), + input_arity=1, + ), + can_add_examples=True, + can_add_nonexamples=True, + z3_translation=lambda a: Z3Template("") + ) + return mult_inv + def create_finite_field_equality_concept(): """Factory function to create the equality concept for finite fields.""" eq = Concept( @@ -581,27 +594,20 @@ def create_finite_field_equality_concept(): ), 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; - """, + z3_translation=lambda a, b: Z3Template("", a, b ) ) # Add examples (reflexive) for i in range(5): - elem = FiniteFieldElement(i) + elem = FiniteFieldElement(DEFAULT_FINITE_FIELD.field(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))) + eq.add_nonexample((FiniteFieldElement(DEFAULT_FINITE_FIELD.field(i)), FiniteFieldElement(DEFAULT_FINITE_FIELD.field(i + 5)))) + eq.add_nonexample((FiniteFieldElement(DEFAULT_FINITE_FIELD.field(i + 5)), FiniteFieldElement(DEFAULT_FINITE_FIELD.field(i)))) + eq.add_nonexample((FiniteFieldElement(DEFAULT_FINITE_FIELD.field(10)), FiniteFieldElement(DEFAULT_FINITE_FIELD.field(20)))) return eq @@ -618,8 +624,10 @@ def create_finite_field_equality_concept(): equality_concept = create_equality_concept() ff_zero_concept = create_finite_field_zero_concept() ff_one_concept = create_finite_field_one_concept() -ff_three_concept = create_finite_field_three_concept() -ff_nine_concept = create_finite_field_nine_concept() +ff_alpha_concept = create_finite_field_alpha_concept() +ff_alpha_squared_concept = create_finite_field_alpha_squared_concept() ff_addition_concept = create_finite_field_addition_concept() ff_multiplication_concept = create_finite_field_multiplication_concept() +ff_additive_inverse_concept = create_finite_field_additive_inverse_concept() +ff_multiplicative_inverse_concept = create_finite_field_multiplicative_inverse_concept() ff_equality_concept = create_finite_field_equality_concept() \ No newline at end of file diff --git a/frame/repl/core/engine.py b/frame/repl/core/engine.py index b91901f..180e553 100644 --- a/frame/repl/core/engine.py +++ b/frame/repl/core/engine.py @@ -145,21 +145,31 @@ def _create_initial_graph(self, domain: str = "ff") -> KnowledgeGraph: graph.add_concept(create_equality_concept()) elif domain == "ff": from frame.knowledge_base.initial_concepts import ( + create_successor_concept, + zero_concept, + create_equality_concept, create_finite_field_zero_concept, create_finite_field_one_concept, - create_finite_field_three_concept, - create_finite_field_nine_concept, + create_finite_field_alpha_concept, + create_finite_field_alpha_squared_concept, create_finite_field_addition_concept, create_finite_field_multiplication_concept, + create_finite_field_additive_inverse_concept, + create_finite_field_multiplicative_inverse_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_three_concept()) - graph.add_concept(create_finite_field_nine_concept()) + graph.add_concept(create_finite_field_alpha_concept()) + graph.add_concept(create_finite_field_alpha_squared_concept()) graph.add_concept(create_finite_field_addition_concept()) graph.add_concept(create_finite_field_multiplication_concept()) + graph.add_concept(create_finite_field_additive_inverse_concept()) + graph.add_concept(create_finite_field_multiplicative_inverse_concept()) graph.add_concept(create_finite_field_equality_concept()) + graph.add_concept(zero_concept) + graph.add_concept(create_successor_concept()) + graph.add_concept(create_equality_concept()) else: raise ValueError(f"Unknown domain for initial graph: {domain}") diff --git a/tests/productions/conftest.py b/tests/productions/conftest.py index acf56d0..097769a 100644 --- a/tests/productions/conftest.py +++ b/tests/productions/conftest.py @@ -988,6 +988,24 @@ def finite_field_of_order_27(): return concept +@pytest.fixture +def add_in_finite_field_of_order_27(): + """Create a concept that adds two elements in the finite field of order 27.""" + concept = Concept( + name="add_in_finite_field_of_order_27", + description="Adds two elements in the finite field of order 27", + computational_implementation=lambda a, b: a + b, + example_structure=ExampleStructure( + concept_type=ConceptType.FUNCTION, + component_types=(ExampleType.FINITEFIELD_ELEMENT, + ExampleType.FINITEFIELD_ELEMENT, + ExampleType.FINITEFIELD_ELEMENT), + input_arity=2, + ), + ) + return concept + + @pytest.fixture def multiply_in_finite_field_of_order_27(): """Create a concept that multiplies two elements in the finite field of order 27.""" @@ -1059,6 +1077,36 @@ def example_primitive_element(): return concept +@pytest.fixture +def zero_in_finite_field_of_order_27(): + """Create a concept that tests if an element is zero in the finite field of order 27.""" + concept = Concept( + name="zero_in_finite_field_of_order_27", + description="Tests if an element is zero in the finite field of order 27", + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(0)), + example_structure=ExampleStructure( + concept_type=ConceptType.CONSTANT, + component_types=(ExampleType.FINITEFIELD_ELEMENT,), + input_arity=0, + ), + ) + return concept + +@pytest.fixture +def one_in_finite_field_of_order_27(): + """Create a concept that tests if an element is one in the finite field of order 27.""" + concept = Concept( + name="one_in_finite_field_of_order_27", + description="Tests if an element is one in the finite field of order 27", + computational_implementation=lambda: FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)), + example_structure=ExampleStructure( + concept_type=ConceptType.CONSTANT, + component_types=(ExampleType.FINITEFIELD_ELEMENT,), + input_arity=0, + ), + ) + return concept + @pytest.fixture def multiply_ff_10_in_finite_field_of_order_27(): """Create a concept that multiplies an element by DEFAULT_FINITE_FIELD(10) in the finite field of order 27.""" diff --git a/tests/productions/test_compose.py b/tests/productions/test_compose.py index cbc9302..77fa346 100644 --- a/tests/productions/test_compose.py +++ b/tests/productions/test_compose.py @@ -271,7 +271,7 @@ def test_function_to_predicate_composition(self, compose_rule, square, is_even): # Test example transformation examples = square_is_even.examples.get_examples() - expected_examples = [(0,), (2,), (4,), (6,)] # Numbers whose square is even + expected_examples = [(0,), (2,), (4,)] # Numbers whose square is even for expected in expected_examples: assert any( ex.value == expected for ex in examples @@ -279,7 +279,7 @@ def test_function_to_predicate_composition(self, compose_rule, square, is_even): # Test nonexample transformation nonexamples = square_is_even.examples.get_nonexamples() - expected_nonexamples = [(1,), (3,), (5,)] # Numbers whose square is odd + expected_nonexamples = [(1,), (3,),] # Numbers whose square is odd for expected in expected_nonexamples: assert any( ex.value == expected for ex in nonexamples diff --git a/tests/productions/test_forall.py b/tests/productions/test_forall.py index fb551cf..8c466c2 100644 --- a/tests/productions/test_forall.py +++ b/tests/productions/test_forall.py @@ -122,10 +122,7 @@ def test_get_valid_parameterizations_complex_case( commutes, multi_arg_predicate ) - # For two predicates, number of indices must match secondary arity (3) - # So we need combinations of size 3 from indices 0,1,2 - # Only [0,1,2] is valid - assert len(valid_params) == NUM_PARAMETERIZATIONS, f"Should return {NUM_PARAMETERIZATIONS} parameterizations but got {len(valid_params)}" + assert len(valid_params) == 0, f"Should return 0 parameterizations due to non-matching types" def test_can_apply_single_predicate(self, forall_rule, is_proper_divisor): """Test that can_apply returns True for valid single predicate case.""" diff --git a/tests/productions/test_specialize.py b/tests/productions/test_specialize.py index 4c12467..a1d5cf0 100644 --- a/tests/productions/test_specialize.py +++ b/tests/productions/test_specialize.py @@ -17,6 +17,7 @@ Zero, Succ, DEFAULT_FINITE_FIELD, + FiniteFieldElement, ) from frame.productions.concepts.specialize import SpecializeRule @@ -227,6 +228,15 @@ def test_specialize_finite_field_element_input(self, ) assert specialized_concept.compute(26), "Primitive element should have order 26" + + def test_specialize_finite_field_add_zero(self, + specialize_rule, add_in_finite_field_of_order_27, zero_in_finite_field_of_order_27): + """Test specializing a finite field element input.""" + specialized_concept = specialize_rule.apply( + add_in_finite_field_of_order_27, zero_in_finite_field_of_order_27, index_to_specialize=0 + ) + + assert specialized_concept.compute(FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1))) == FiniteFieldElement(DEFAULT_FINITE_FIELD.field(1)) # ============================== # Output Specialization Tests