# Mutually inductive/bidirectional evaluation contexts

Define a simple bidirectional lambda calculus grammar and types

$$\tau \mathrel{::=} \Box \mid \tau \rightarrow$$

$$M \mathrel{::=} \lambda x. M \mid [R]$$ $$R \mathrel{::=} x \mid R M \mid M\colon \tau$$

$$\frac{\Gamma, x\colon \tau \vdash M \Leftarrow \tau'}{\Gamma \vdash \lambda x. M \Leftarrow \tau \rightarrow \tau' }$$ $$\frac{\Gamma \vdash R \Rightarrow \tau}{\Gamma \vdash [ R] \Leftarrow \tau}$$ $$\frac{x \colon \tau \in \Gamma}{\Gamma \vdash x \Rightarrow \tau}$$ $$\frac{\begin{split}\Gamma \vdash R \Rightarrow \tau \rightarrow \tau'\\ \Gamma \vdash M \Rightarrow \tau \end{split}}{\Gamma \vdash RM \Rightarrow \tau'}$$ $$\frac{\Gamma \vdash M \Leftarrow \tau}{\Gamma \vdash M \colon \tau \Rightarrow \tau}$$

There are many ways to give an operational semantics to this.

I was curious how one would use evaluation contexts here.

I feel like the most naive interpretation using the intuition of a one hole context as a derivative would define two sets of contexts something like

$$\frac{\partial M}{\partial M} \mathrel{::=} \lambda x. \_ \mid \left[\frac{\partial R}{\partial M} \right]$$ $$\frac{\partial R}{\partial M} \mathrel{::=} \frac{\partial R}{\partial M} M \mid R \_ \mid \_\colon \tau$$

$$\frac{\partial M}{\partial R} \mathrel{::=} \lambda x. \frac{\partial M}{\partial R} \mid [\_]$$ $$\frac{\partial R}{\partial R} \mathrel{::=} \_ M \mid R \frac{\partial M}{\partial R} \mid \frac{\partial M}{\partial R} \colon \tau$$

And then you would have a bunch of small step rules like

$$\frac{R \longrightarrow R'}{\frac{\partial M}{\partial R} [R] \longrightarrow \frac{\partial M}{\partial R}[R']}$$

But this seems very funky on top of prosaic concerns like figuring out what to name all the separate evaluation contexts.

• I'm not sure if you are talking about bidirectional type-checking (which can be seen as a form of removing non-determinism from a relation) or bidirectional computing, where you can, crudely put, run a computation backwards. Apr 27, 2022 at 10:02