Lifetime Projections

Lifetime projections take the following form

$$\begin{array}{llr}rp& ::=& \text{(Lifetime Projection)}\\ & \mid \hat{p}\downarrow r& \text{(Place Projection)}\\ & \mid \hat{p}\downarrow r\text{at}\ell & \text{(Snapshot of Place Projection)}\\ & \mid \hat{p}\downarrow r\text{at}\text{FUTURE}& \text{(Placeholder Projection)}\\ & \mid c\downarrow r& \text{(Constant Projection)}\end{array}$$

Lifetime Projection Lifetime

The lifetime $r(rp)$ of a lifetime projection $rp$ is conceptually the lifetime $r$ on the right of the $\downarrow$, i.e:

• $r(\hat{p}\downarrow r)=r$
• $r(\hat{p}\downarrow r\text{at}\ell )=r$
• $r(\hat{p}\downarrow r\text{at}\text{FUTURE})=r$
• $r(c\downarrow r)=r$

Lifetime Projection Base

The base $base(rp)$ of a lifetime projection $rp$ is conceptually the part on the left of the $\downarrow$, i.e. defined as follows:

• $base(\hat{p}\downarrow r)=\hat{p}$
• $base(\hat{p}\downarrow r\text{at}\ell )=\hat{p}$
• $base(\hat{p}\downarrow r\text{at}\text{FUTURE})=\hat{p}$
• $base(c\downarrow r)=c$