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

Question

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

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)

Answer 1

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:

• When v2 is a value, then a lambda application (\x : T2 . t1) v2 reduces to t1 with x in t1 substituted by v2. (That's Beta reduction)
• When t1 reduces to t1', then the application t1 t2 reduces to t1' t2.
• When v1 is a value, and t2 reduces to t2', then the application v1 t2 reduces to v1 t2'.

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