typesfunctional-programminglambda-calculustyped-lambda-calculus

What are the weird equations found while researching Simply Typed Lambda Calculus


I was learning about the Simply Typed Lambda Calculus but I have gotten confused over these sorts of equations.

enter image description here

I wanted to know what they were called and how they work.

Thanks for your help!

(image taken from https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html)


Solution

  • They are usually just called deduction rules, typing rules, or, in general, inference rules. The notation with the inference bar is AFAIK due to Gentzen's usage in natural deduction.

    The exact interpretation depends on the system you're describing, but the general idea is "the conditions on the top imply/allow the things on the bottom". In this specific case, it doesn't really look that formal, but good enough if you have seen this kind of stuff before. See here for a more formal "semantics" of what type theory people usually write.

    In you specific case, I'd translate the rules as:

    So in this case, they are actually not typing rules, but the rules for how evaluation (reduction) works.