Add support for finite fields

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" 

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}),
+    ),
+} 

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",
+    ),
+} 

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;
+        """)
+    ),
+} 

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:

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