0
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$ Apr 27, 2022 at 10:02

0

Your Answer

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

Browse other questions tagged or ask your own question.