Change notation for types, substitutions and instantiations

code/notebook/math/lambda_/conftest.py

@@ -5,4 +5,4 @@
 
 @pytest.fixture
 def dummy_signature() -> LambdaSignature:
-    return LambdaSignature(base_types={'α', 'β', 'γ'}, constant_terms=set())
+    return LambdaSignature(base_types={'τ', 'σ', 'ρ'}, constant_terms=set())

code/notebook/math/lambda_/instantiation/test_term_application.py

@@ -78,19 +78,19 @@ def test_term_instantiation_failure() -> None:
 
 
 def test_abstraction_annotation_success() -> None:
-    schema = parse_pure_term_schema('(λx:α.x)', TypingStyle.explicit)
+    schema = parse_pure_term_schema('(λx:τ.x)', TypingStyle.explicit)
     instantiation = LambdaSchemaInstantiation(
         variable_mapping={parse_variable_placeholder('x'): parse_variable('x')},
-        type_mapping={parse_type_placeholder('α'): parse_type(HOL_SIGNATURE, 'ι')}
+        type_mapping={parse_type_placeholder('τ'): parse_type(HOL_SIGNATURE, 'ι')}
     )
 
     expected = parse_term(HOL_SIGNATURE, '(λx:ι.x)', TypingStyle.explicit)
     assert instantiate_term_schema(schema, instantiation) == expected
 
 
 def test_abstraction_annotation_failure() -> None:
-    with pytest.raises(SchemaInstantiationError, match=r'No specification of how to instantiate the type placeholder α'):
-        schema = parse_pure_term_schema('(λx:α.x)', TypingStyle.explicit)
+    with pytest.raises(SchemaInstantiationError, match=r'No specification of how to instantiate the type placeholder τ'):
+        schema = parse_pure_term_schema('(λx:τ.x)', TypingStyle.explicit)
         instantiation = LambdaSchemaInstantiation(
             variable_mapping={parse_variable_placeholder('x'): parse_variable('x')},
         )
@@ -104,19 +104,19 @@ def test_typed_instantiation_on_untyped_schema() -> None:
         instantiation = LambdaSchemaInstantiation(
             variable_mapping={parse_variable_placeholder('x'): parse_variable('x')},
             term_mapping={parse_term_placeholder('M'): parse_term(HOL_SIGNATURE, '(λy:ι.y)', TypingStyle.explicit)},
-            type_mapping={parse_type_placeholder('α'): parse_type(HOL_SIGNATURE, 'ι')}
+            type_mapping={parse_type_placeholder('τ'): parse_type(HOL_SIGNATURE, 'ι')}
         )
 
         instantiate_term_schema(schema, instantiation)
 
 
 def test_untyped_instantiation_on_typed_schema() -> None:
     with pytest.raises(SchemaInstantiationError, match='A typed schema was provided, but the instantiation features untyped terms'):
-        schema = parse_pure_term_schema('(λx:α.M)', TypingStyle.explicit)
+        schema = parse_pure_term_schema('(λx:τ.M)', TypingStyle.explicit)
         instantiation = LambdaSchemaInstantiation(
             variable_mapping={parse_variable_placeholder('x'): parse_variable('x')},
             term_mapping={parse_term_placeholder('M'): parse_term(HOL_SIGNATURE, '(λy.y)', TypingStyle.implicit)},
-            type_mapping={parse_type_placeholder('α'): parse_type(HOL_SIGNATURE, 'ι')}
+            type_mapping={parse_type_placeholder('τ'): parse_type(HOL_SIGNATURE, 'ι')}
         )
 
         instantiate_term_schema(schema, instantiation)

code/notebook/math/lambda_/instantiation/test_term_inference.py

@@ -109,18 +109,18 @@ def test_abstraction_instantiation_failure() -> None:
 
 
 def test_abstraction_annotation_success() -> None:
-    schema = parse_pure_term_schema('(λx:α.x)', TypingStyle.explicit)
+    schema = parse_pure_term_schema('(λx:τ.x)', TypingStyle.explicit)
     term = parse_term(HOL_SIGNATURE, '(λx:ι.x)', TypingStyle.explicit)
     assert infer_instantiation_from_term(schema, term) == LambdaSchemaInstantiation(
         variable_mapping={parse_variable_placeholder('x'): parse_variable('x')},
-        type_mapping={parse_type_placeholder('α'): parse_type(HOL_SIGNATURE, 'ι')}
+        type_mapping={parse_type_placeholder('τ'): parse_type(HOL_SIGNATURE, 'ι')}
     )
 
 
 def test_abstraction_annotation_failure() -> None:
-    with pytest.raises(SchemaInferenceError, match=r'The schema \(λx:α.x\) has a type annotation on its abstractor, but the term \(λx.x\) does not'):
+    with pytest.raises(SchemaInferenceError, match=r'The schema \(λx:τ.x\) has a type annotation on its abstractor, but the term \(λx.x\) does not'):
         infer_instantiation_from_term(
-            parse_pure_term_schema('(λx:α.x)', TypingStyle.explicit),
+            parse_pure_term_schema('(λx:τ.x)', TypingStyle.explicit),
             parse_pure_term('(λx.x)')
         )
 

code/notebook/math/lambda_/parsing/test_parser.py

@@ -241,10 +241,10 @@ def test_parsing_valid_type(type_: str, expected: SimpleType) -> None:
     schema=[
         'ι',
         '(ι → o)',
-        'α',
-        '(β → β)',
-        '(ι → (α → β))',
-        '((ι → α) → β)'
+        'τ',
+        '(σ → σ)',
+        '(ι → (τ → σ))',
+        '((ι → τ) → σ)'
     ]
 )
 def test_rebuilding_type_schema(schema: str) -> None:
@@ -253,11 +253,11 @@ def test_rebuilding_type_schema(schema: str) -> None:
 
 def test_parsing_type_schema_with_regular_parser() -> None:
     with pytest.raises(ParsingError) as excinfo:
-        parse_type(HOL_SIGNATURE, 'α')
+        parse_type(HOL_SIGNATURE, 'τ')
 
     assert str(excinfo.value) == 'Type placeholders are only allowed in schemas'
     assert excinfo.value.__notes__[0] == dedent('''\
-        1 │ α
+        1 │ τ
           │ ^
         '''
     )
@@ -337,10 +337,10 @@ def test_parsing_type_assertion_missing_colon() -> None:
 
 @pytest_parametrize_lists(
     rule=[
-        '(R) ⫢ x: α',
-        '(R) M: (α → β), N: α ⫢ (MN): β',
-        '(R) [x: α] M: β ⫢ (λx.M): (α → β)',
-        '(R) [x: α] M: β ⫢ (λx:α.M): (α → β)'
+        '(R) ⫢ x: τ',
+        '(R) M: (τ → σ), N: τ ⫢ (MN): σ',
+        '(R) [x: τ] M: σ ⫢ (λx.M): (τ → σ)',
+        '(R) [x: τ] M: σ ⫢ (λx:τ.M): (τ → σ)'
     ]
 )
 def test_rebuilding_typing_rules(rule: str) -> None:
@@ -349,23 +349,23 @@ def test_rebuilding_typing_rules(rule: str) -> None:
 
 def test_parsing_discharge_schema_with_no_name() -> None:
     with pytest.raises(ParsingError) as excinfo:
-        parse_typing_rule(EMPTY_SIGNATURE, '(R) [] x: α ⫢ y: α', TypingStyle.implicit)
+        parse_typing_rule(EMPTY_SIGNATURE, '(R) [] x: τ ⫢ y: τ', TypingStyle.implicit)
 
     assert str(excinfo.value) == 'Unexpected token'
     assert excinfo.value.__notes__[0] == dedent('''\
-        1 │ (R) [] x: α ⫢ y: α
+        1 │ (R) [] x: τ ⫢ y: τ
           │      ^
         '''
     )
 
 
 def test_parsing_discharge_schema_with_no_closing_bracket() -> None:
     with pytest.raises(ParsingError) as excinfo:
-        parse_typing_rule(EMPTY_SIGNATURE, '(R) [x: α y: α ⫢ z: α', TypingStyle.implicit)
+        parse_typing_rule(EMPTY_SIGNATURE, '(R) [x: τ y: τ ⫢ z: τ', TypingStyle.implicit)
 
     assert str(excinfo.value) == 'Unclosed bracket for discharge schema'
     assert excinfo.value.__notes__[0] == dedent('''\
-        1 │ (R) [x: α y: α ⫢ z: α
+        1 │ (R) [x: τ y: τ ⫢ z: τ
           │     ^^^^^^
         '''
     )

code/notebook/math/lambda_/reduction/strategies.py

@@ -21,7 +21,7 @@ def reduce_term_once(term: UntypedTerm, strategy: ReductionStrategy) -> UntypedT
     reduction = strategy.try_reduce(term)
 
     if reduction is None:
-        raise ReductionError(f'Cannot β-reduce {reduction}')
+        raise ReductionError(f'Cannot σ-reduce {reduction}')
 
     return reduction
 

code/notebook/math/lambda_/type_derivation/test_inference.py

@@ -8,41 +8,41 @@
 
 # ex:def:type_derivation_tree/i
 def test_arrow_intro(dummy_signature: LambdaSignature) -> None:
-    term = parse_term(dummy_signature, '(λx:α.x)', TypingStyle.explicit)
+    term = parse_term(dummy_signature, '(λx:τ.x)', TypingStyle.explicit)
     assert str(derive_type(term)) == dedent('''\
-               x: α
+               x: τ
         x _________________ →⁺
-          (λx:α.x): (α → α)
+          (λx:τ.x): (τ → τ)
         '''
     )
 
 
 def test_nested_arrow_intro(dummy_signature: LambdaSignature) -> None:
-    term = parse_term(dummy_signature, '(λx:α.(λy:β.x))', TypingStyle.explicit)
+    term = parse_term(dummy_signature, '(λx:τ.(λy:σ.x))', TypingStyle.explicit)
     assert str(derive_type(term)) == dedent('''\
-                     x: α
+                     x: τ
                 _________________ →⁺
-                (λy:β.x): (β → α)
+                (λy:σ.x): (σ → τ)
         x ______________________________ →⁺
-          (λx:α.(λy:β.x)): (α → (β → α))
+          (λx:τ.(λy:σ.x)): (τ → (σ → τ))
         '''
     )
 
 
 # ex:def:type_derivation_tree/pairs
 def test_cons(dummy_signature: LambdaSignature) -> None:
-    term = parse_term(dummy_signature, '(λx:α.(λy:β.(λf:(α→(β→γ)).((fx)y))))', TypingStyle.explicit)
+    term = parse_term(dummy_signature, '(λx:τ.(λy:σ.(λf:(τ→(σ→ρ)).((fx)y))))', TypingStyle.explicit)
     assert str(derive_type(term)) == dedent('''\
-                         f: (α → (β → γ))      x: α
+                         f: (τ → (σ → ρ))      x: τ
                          ____________________________ →⁻
-                                (fx): (β → γ)               y: β
+                                (fx): (σ → ρ)               y: σ
                          _________________________________________ →⁻
-                                        ((fx)y): γ
+                                        ((fx)y): ρ
                     f _______________________________________________ →⁺
-                      (λf:(α → (β → γ)).((fx)y)): ((α → (β → γ)) → γ)
+                      (λf:(τ → (σ → ρ)).((fx)y)): ((τ → (σ → ρ)) → ρ)
               y ____________________________________________________________ →⁺
-                (λy:β.(λf:(α → (β → γ)).((fx)y))): (β → ((α → (β → γ)) → γ))
+                (λy:σ.(λf:(τ → (σ → ρ)).((fx)y))): (σ → ((τ → (σ → ρ)) → ρ))
         x _________________________________________________________________________ →⁺
-          (λx:α.(λy:β.(λf:(α → (β → γ)).((fx)y)))): (α → (β → ((α → (β → γ)) → γ)))
+          (λx:τ.(λy:σ.(λf:(τ → (σ → ρ)).((fx)y)))): (τ → (σ → ((τ → (σ → ρ)) → ρ)))
         '''
     )

code/notebook/math/lambda_/type_derivation/test_tree.py

@@ -8,18 +8,18 @@
 
 
 def test_assumption_tree(dummy_signature: LambdaSignature) -> None:
-    assumption = parse_variable_assertion(dummy_signature, 'x: α')
+    assumption = parse_variable_assertion(dummy_signature, 'x: τ')
     tree = assume(assumption)
     assert tree.get_context() == {assumption}
     assert str(tree) == dedent('''\
-        x: α
+        x: τ
         '''
     )
 
 
 # ex:def:type_derivation_tree/i
 def test_arrow_intro_untyped(dummy_signature: LambdaSignature) -> None:
-    assumption = parse_variable_assertion(dummy_signature, 'x: α')
+    assumption = parse_variable_assertion(dummy_signature, 'x: τ')
     tree = apply(
         ARROW_INTRO_RULE_IMPLICIT,
         RuleApplicationPremise(
@@ -31,16 +31,16 @@ def test_arrow_intro_untyped(dummy_signature: LambdaSignature) -> None:
     assert tree.get_context() == set()
     assert tree.conclusion.term == combinators.i
     assert str(tree) == dedent('''\
-              x: α
+              x: τ
         x _______________ →⁺
-          (λx.x): (α → α)
+          (λx.x): (τ → τ)
         '''
     )
 
 
 # ex:def:type_derivation_tree/i
 def test_arrow_intro_typed(dummy_signature: LambdaSignature) -> None:
-    assumption = parse_variable_assertion(dummy_signature, 'x: α')
+    assumption = parse_variable_assertion(dummy_signature, 'x: τ')
     tree = apply(
         ARROW_INTRO_RULE_EXPLICIT,
         RuleApplicationPremise(
@@ -51,17 +51,17 @@ def test_arrow_intro_typed(dummy_signature: LambdaSignature) -> None:
 
     assert tree.get_context() == set()
     assert str(tree) == dedent('''\
-               x: α
+               x: τ
         x _________________ →⁺
-          (λx:α.x): (α → α)
+          (λx:τ.x): (τ → τ)
         '''
     )
 
 
 # ex:def:type_derivation_tree/k
 def test_nested_arrow_intro(dummy_signature: LambdaSignature) -> None:
-    assumption_x = parse_variable_assertion(dummy_signature, 'x: α')
-    assumption_y = parse_variable_assertion(dummy_signature, 'y: β')
+    assumption_x = parse_variable_assertion(dummy_signature, 'x: τ')
+    assumption_y = parse_variable_assertion(dummy_signature, 'y: σ')
     tree = apply(
         ARROW_INTRO_RULE_IMPLICIT,
         RuleApplicationPremise(
@@ -79,20 +79,20 @@ def test_nested_arrow_intro(dummy_signature: LambdaSignature) -> None:
     assert tree.get_context() == set()
     assert tree.conclusion.term == combinators.k
     assert str(tree) == dedent('''\
-                   x: α
+                   x: τ
                _______________ →⁺
-               (λy.x): (β → α)
+               (λy.x): (σ → τ)
         x __________________________ →⁺
-          (λx.(λy.x)): (α → (β → α))
+          (λx.(λy.x)): (τ → (σ → τ))
         '''
     )
 
 
 # ex:def:type_derivation_tree/pairs
 def test_cons(dummy_signature: LambdaSignature) -> None:
-    assumption_f = parse_variable_assertion(dummy_signature, 'f: (α → (β → γ))')
-    assumption_x = parse_variable_assertion(dummy_signature, 'x: α')
-    assumption_y = parse_variable_assertion(dummy_signature, 'y: β')
+    assumption_f = parse_variable_assertion(dummy_signature, 'f: (τ → (σ → ρ))')
+    assumption_x = parse_variable_assertion(dummy_signature, 'x: τ')
+    assumption_y = parse_variable_assertion(dummy_signature, 'y: σ')
     tree = apply(
         ARROW_INTRO_RULE_IMPLICIT,
         RuleApplicationPremise(
@@ -126,16 +126,16 @@ def test_cons(dummy_signature: LambdaSignature) -> None:
     assert tree.get_context() == set()
     assert tree.conclusion.term == pairs.cons
     assert str(tree) == dedent('''\
-                f: (α → (β → γ))      x: α
+                f: (τ → (σ → ρ))      x: τ
                 ____________________________ →⁻
-                       (fx): (β → γ)               y: β
+                       (fx): (σ → ρ)               y: σ
                 _________________________________________ →⁻
-                               ((fx)y): γ
+                               ((fx)y): ρ
               f _________________________________________ →⁺
-                    (λf.((fx)y)): ((α → (β → γ)) → γ)
+                    (λf.((fx)y)): ((τ → (σ → ρ)) → ρ)
              y ____________________________________________ →⁺
-               (λy.(λf.((fx)y))): (β → ((α → (β → γ)) → γ))
+               (λy.(λf.((fx)y))): (σ → ((τ → (σ → ρ)) → ρ))
         x _______________________________________________________ →⁺
-          (λx.(λy.(λf.((fx)y)))): (α → (β → ((α → (β → γ)) → γ)))
+          (λx.(λy.(λf.((fx)y)))): (τ → (σ → ((τ → (σ → ρ)) → ρ)))
         '''
     )

code/notebook/math/lambda_/type_systems/base.py

@@ -4,9 +4,9 @@
 
 
 # These rules are distinct
-ARROW_INTRO_RULE_IMPLICIT = parse_typing_rule(EMPTY_SIGNATURE, '(→⁺) [x: α] M: β ⫢ (λx.M): (α → β)', TypingStyle.implicit)
-ARROW_INTRO_RULE_EXPLICIT = parse_typing_rule(EMPTY_SIGNATURE, '(→⁺) [x: α] M: β ⫢ (λx:α.M): (α → β)', TypingStyle.explicit)
+ARROW_INTRO_RULE_IMPLICIT = parse_typing_rule(EMPTY_SIGNATURE, '(→⁺) [x: τ] M: σ ⫢ (λx.M): (τ → σ)', TypingStyle.implicit)
+ARROW_INTRO_RULE_EXPLICIT = parse_typing_rule(EMPTY_SIGNATURE, '(→⁺) [x: τ] M: σ ⫢ (λx:τ.M): (τ → σ)', TypingStyle.explicit)
 
 # These rules are identical, but belong to different classes
-ARROW_ELIM_RULE_IMPLICIT = parse_typing_rule(EMPTY_SIGNATURE, '(→⁻) M: (α → β), N: α ⫢ (MN): β', TypingStyle.implicit)
-ARROW_ELIM_RULE_EXPLICIT = parse_typing_rule(EMPTY_SIGNATURE, '(→⁻) M: (α → β), N: α ⫢ (MN): β', TypingStyle.explicit)
+ARROW_ELIM_RULE_IMPLICIT = parse_typing_rule(EMPTY_SIGNATURE, '(→⁻) M: (τ → σ), N: τ ⫢ (MN): σ', TypingStyle.implicit)
+ARROW_ELIM_RULE_EXPLICIT = parse_typing_rule(EMPTY_SIGNATURE, '(→⁻) M: (τ → σ), N: τ ⫢ (MN): σ', TypingStyle.explicit)

code/notebook/support/test_unicode.py

@@ -56,7 +56,7 @@ def test_is_latin_string_capitaliation(string: str = 'abc') -> None:
         assert xnor(Capitalization.mixed in cap, is_latin_string(mixed, capitalization=cap))
 
 
-def test_is_greek_string_capitaliation(string: str = 'αβγ') -> None:
+def test_is_greek_string_capitaliation(string: str = 'τσρ') -> None:
     lower = string.lower()
     upper = string.upper()
     mixed = string.title()

code/notebook/support/unicode.py

@@ -146,7 +146,7 @@ def is_latin_string(string: str, capitalization: Capitalization) -> bool:
 def is_greek_string(string: str, capitalization: Capitalization) -> bool:
     return all(
         ('Α' <= c <= 'Ω' if Capitalization.upper in capitalization else False) or
-        ('α' <= c <= 'ω' if Capitalization.lower in capitalization else False)
+        ('τ' <= c <= 'ω' if Capitalization.lower in capitalization else False)
         for c in string
     )
 

figures/ex__def__propositional_formula_ast.tex

@@ -22,7 +22,7 @@
         [
           \( \synwedge \)
             [\( \synq \)]
-            [\( \syn r \)]
+            [\( \synr \)]
         ]
     ]
   \end{forest}
@@ -35,7 +35,7 @@
             [\( \synp \)]
             [\( \synq \)]
         ]
-        [\( \syn r \)]
+        [\( \synr \)]
     ]
   \end{forest}
 \end{document}