1

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)

Glubs
  • 106
  • 1
  • 7
  • they describe a reduction algorithm: in AB, if A is a lambda term and B is irreducible (i.e. a "value"), perform the substitution ; otherwise try reducing A-->A' and then the result is A'B; otherwise (when A is irreducible i.e. a "value") try reducing B-->B' and then the result is AB'. continue applying these rules until none more applies, then you have the final result. IOW, to perform an application AB, simplify A as much as possible, then simplify B as much as possible, then provided you got a Lambda term as new A', perform the substitution. – Will Ness Sep 07 '20 at 12:33

1 Answers1

4

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.

phipsgabler
  • 20,535
  • 4
  • 40
  • 60