In Harper's PFPL (Ed. 2, top of page 8), this notation is used but I don't see a definition. What does $x.y$ mean?
1 Answer
$\begingroup$
$\endgroup$
This is the notation for Harper's "abstract binding structures": x.t represents the binding site of a variable x and the term t the variable scopes over.
Apparently you are in the parts that define variable bindings. $\mathcal{B}[\mathcal{X}]_s$ appears to be the set of terms, or binding structures at sort $s$ whose free variables are among $\mathcal{X}$. So I would expect (but I don't have the book) that there is in fact an explanation for this notation close by.
