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)
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:
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)t1
reduces to t1'
, then the application t1 t2
reduces to t1' t2
.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.