What's the Meaning of the Notation $ \langle \mathbf{\cdot} , \mathbf{\cdot} \rangle$ in $\lambda$-Calculus?

66 Views Asked by At

I'm learning $\lambda$-calculus from this book: Lectures on the Curry-Howard Isomorphism (1998 version) (https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf), and in page 17, definition 1.5.21 the symbol $ \langle \mathbf{\cdot} , \mathbf{\cdot} \rangle$ appears. I'm not familiar with this symbol, what does it mean?

2

There are 2 best solutions below

2
On BEST ANSWER

As the definition states, it denotes an arbitrary "bijective, recursive function" from $\Bbb N^2$ to $\Bbb N$. In terms of $\langle\bullet,\,\bullet\rangle$, it defines a map $\#$. You may want to see, for example, what this does for the Cantor pairing function.

0
On

It is an internal notation which is precisely defined on the page you refer to:

Let $\left< \cdot,\cdot \right>:\Bbb N^2\to \Bbb N$ be a bijective, recursive function.

The word recursive in this context is defined on page $15$, Def. 1.5.15.