# What does this typed lambda-calculus notation mean?

In Definition 3.2 (page 12) of Gallier's 'Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi' he sets out the rules for his typed $$\lambda^{\to, +, \times, \perp}$$-calculus. I've studied simply typed $$\lambda$$-calculus before so understand most of what he's saying, however was unsure about a few bits of notation, and couldn't find a definition (or intended interpretation) anywhere in the text/online. (I've switched Gallier's $$\rhd$$ for $$\vdash$$ as it's what I'm more used to.)

1. First in $$\perp$$-elim, the use of $$\nabla$$: $$\frac{\Gamma \vdash M:\perp}{\Gamma \vdash \nabla_A(M): A}$$

2. Then in the 'by cases' rule, the use of $$\texttt{case}$$: $$\frac{\Gamma \vdash P : A + B \quad \Gamma, x:A \vdash M : C \quad \Gamma, y : B \vdash N : C} {\Gamma \vdash \texttt{case}(P, \lambda x: A.M, \lambda y: B.N) : C}$$

Any help/clarification appreciated.

• No hint in the Lecture of what the "inverted Delta"(M) means? Dec 23, 2021 at 14:34

These are the definitions of $$\nabla_A$$ and $$\texttt{case}$$. These are freely defined constructors of type $$\nabla_A : \bot\to A$$ and $$\texttt{case} : A + B\to (A\to C) \to (B \to C) \to C.$$ They don't reduce to anything. They are simply the proof constructors corresponding to elimination of $$\bot$$ and $$+$$.