<p>This is the notation for Harper's &quot;abstract binding structures&quot;: <code>x.t</code> represents the binding site of a variable <code>x</code> and the term <code>t</code> the variable scopes over.</p>
<p>Apparently you are in the parts that define variable bindings. <span class="math-container">$\mathcal{B}[\mathcal{X}]_s$</span> appears to be the set of terms, or binding structures at sort <span class="math-container">$s$</span> whose free variables are among <span class="math-container">$\mathcal{X}$</span>. So I would expect (but I don't have the book) that there is in fact an explanation for this notation close by.</p>

CC BY-SA 4.0
2021-05-09T05:15:45.387Z
2021-05-09T05:15:45.387Z
gasche
<p><a href="https://i.sstatic.net/4ZmNt.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/4ZmNt.png" alt="enter image description here" /></a></p>
<p>In Harper's PFPL (Ed. 2, top of page 8), this notation is used but I don't see a definition. What does <span class="math-container">$x.y$</span> mean?</p>

<pl.programming-languages><notation>
What does x.y notation mean?
andi
# What does x.y notation mean?

(Asked by: username_0 on 2021-05-08)

[![enter image description here](https://i.sstatic.net/4ZmNt.png)](https://i.sstatic.net/4ZmNt.png)

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?

**Tags:** pl.programming-languages, notation

---

## 1 answers

### Answer by username_1 on 2021-05-09. Score: 3 | Accepted answer

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.


---

