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.