strangerRidingCaml
4. Introduction to Inference Rules and Typing Rules 본문
Introduction to Inference Rules and Typing Rules
Inference rules and typing rules are fundamental components of formal systems used to derive conclusions about the behavior and properties of expressions.
Inference rules are logical rules that specify how new knowledge or conclusions can be derived from existing premises or assumptions.
They are typically expressed as a set of premises leading to a conclusion, and are used to make deductions in a formal system.
Typing rules are a specific type of inference rule used in type systems to determine the types of expressions.
In a type system, each term is associated with a type, and typing rules specify how to infer the type of a term based on its structure and context.
For example, in a simple type system, we might have typing rules such as:
T-Var: Γ(x) = τ
-------------------
Γ ⊢ x : τ
T-Abs: Γ, x:τ₁ ⊢ e : τ₂
--------------------------
Γ ⊢ (λx:τ₁. e) : (τ₁ → τ₂)
These typing rules specify how to infer the type of a variable (`T-Var`) and a lambda abstraction (`T-Abs`).
Lab Activity: Implementing Typing Rules
Let's implement a basic type checker in Python using inference rules and typing rules.
class Term:
def __init__(self, term, term_type):
self.term = term
self.term_type = term_type
def type_check(term, context):
if term.term == "var":
var_name = term.term_type
if var_name in context:
return context[var_name]
else:
raise ValueError("Variable not found in context")
elif term.term == "abs":
var_name, var_type, body = term.term_type
new_context = context.copy()
new_context[var_name] = var_type
body_type = type_check(body, new_context)
return ("->", var_type, body_type)
elif term.term == "app":
abs_term, arg_term = term.term_type
abs_type = type_check(abs_term, context)
arg_type = type_check(arg_term, context)
if abs_type[0] == "->" and abs_type[1] == arg_type:
return abs_type[2]
else:
raise ValueError("Type mismatch in application")
else:
raise ValueError("Unknown term")
def main():
context = {"x": "Bool"}
term = Term("abs", ("x", "Bool", Term("var", "x")))
try:
result = type_check(term, context)
print("Type:", result)
except ValueError as e:
print("Error:", e)
if __name__ == "__main__":
main()
In the lab activity, we define a `Term` class to represent lambda expressions along with their types.
The `type_check` function performs type checking using typing rules, recursively traversing the lambda expression.
We then test the implementation with a sample lambda expression and observe the inferred type.
'Type theory' 카테고리의 다른 글
6. Polymorphism and Parametric Polymorphism (0) | 2024.05.10 |
---|---|
5. Type Safety: Progress and Preservation Theorems (0) | 2024.05.10 |
3. Simply Typed Lambda Calculus (STLC) (0) | 2024.05.10 |
2. Basic Concepts of Type Theory (0) | 2024.05.10 |
1. Type Theory Overview (0) | 2024.05.10 |