0
$\begingroup$

enter image description here

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?

$\endgroup$
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.