3. Simply Typed Lambda Calculus (STLC)

Simply Typed Lambda Calculus (STLC)

The Simply Typed Lambda Calculus (STLC) is a foundational formal system in lambda calculus with typed expressions.

In STLC, each lambda abstraction is annotated with a specific type, and the application of functions is type-checked to ensure type compatibility.

The syntax of STLC includes terms, types, and typing judgments.

Terms are represented as lambda abstractions, variables, and function applications.

For example, a term in STLC can be expressed as:

λx: T. x

Where λx: T. x represents a lambda abstraction with parameter x of type T returning x.

Types in STLC include basic types like Boolean, Integer, and Function, as well as function types.

A type judgment in STLC has the form term : type, indicating that the given term has the specified type.

Lab Activity: Implementing Simply Typed Lambda Calculus

Let's implement a simple interpreter for Simply Typed Lambda Calculus in Python.

class Term:
    def __init__(self, term, term_type):
        self.term = term
        self.term_type = term_type

def type_check(term):
    # Type checking logic
    pass

def eval(term):
    # Evaluation logic
    pass

def main():
    term = Term("λx: Bool. x", "Bool")
    try:
        result_type = type_check(term)
        print("Type:", result_type)
        result = eval(term)
        print("Result:", result)
    except Exception 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 on the given term, ensuring that lambda abstractions and applications are well-typed.

The `eval` function evaluates the lambda expression based on its type.

We then test the implementation with a sample term and observe the type and evaluation result.