notesum.ai

Published at November 21

Datalog with First-Class Facts

cs.DB

cs.PL

Released Date: November 21, 2024

Authors: Thomas Gilray¹, Arash Sahebolamri², Yihao Sun, Sowmith Kunapaneni¹, Sidharth Kumar³, Kristopher Micinski

Aff.: ¹Washington State University; ²Syracuse University; ³University of Illinois at Chicago

Arxiv: http://arxiv.org/abs/2411.14330v1

Var ${\frac{v\,=\,\rho(x)}{x,\rho\ \Downarrow\ v}}$	$\Downarrow\!(\textit{call},\ v)\ \leftarrow$ $\textit{call}\ =\ \textit{eval}(\textit{ref}(x),\rho),$ $\_\!=\!\textit{lookup}(\rho,\ x,\ v)$
Abs ${\frac{}{(\lambda\,(x)\,e),\rho\ \Downarrow\ \langle(\lambda\,(x)\,e),\rho% \rangle}}$	$\Downarrow\!(\textit{call},\ \textit{clo}(\textit{lam},\ \rho))\ \leftarrow$ $\textit{call}\ =\ \textit{eval}(\textit{lam},\rho),$ $\textit{lam}\ =\ \lambda(x,\ e)$
App ${\frac{\overset{{e_{f},\rho\Downarrow\langle(\lambda\,(x)\,e_{b}),\rho_{% \lambda}\rangle}}{e_{a},\rho\Downarrow v_{a}\quad e_{b},\rho_{\lambda}[x% \mapsto v_{a}]\Downarrow v}}{(e_{f}~{}e_{a}),\rho\ \Downarrow\ v}}$	$\Downarrow\!(\textit{call},\ v)\ \leftarrow$ $\textit{call}\ =\ \textit{eval}(\textit{app}(e_f\,e_a),\ \rho),$ $\_\!=\,\Downarrow\!(\textit{eval}(e_f,\rho),$ $\textit{clo}(\lambda(x,e_b),\ \rho_\lambda)),$ $\_\!=\,\Downarrow\!(\textit{eval}(e_a,\rho),\ v_a),$ $\_\ =\,\Downarrow\!(\textit{eval}(e_b,\rho^{\prime},\ v),$ $\rho^{\prime}\ =\ \mapsto\!\!(\rho_\lambda,\ x,\ v_a))$
Defunctionalized Environments $\textit{lookup}(\rho,\ x,\ v)\ \leftarrow\$ $\rho\ =\ \mapsto\!\!(\_,\ x,\ v)$ $\textit{lookup}(\rho,\ x,\ v)\ \leftarrow\$ $\rho\ =\ \mapsto\!\!(\rho^{\prime},\ y,\ \_),$ $x\ \neq\ y,$ $\textit{lookup}(\rho^{\prime},\ x,\ v)$	$\textit{eval}(e_f,\rho),\ \textit{eval}(e_a,\rho)\ \leftarrow$ $\_\!=\!\textit{eval}(\textit{app}(e_f\,e_a),\ \rho)$ $\textit{eval}(e_b,\mapsto\!\!(\rho_\lambda,\ x,\ v_a))\ \leftarrow$ $\_\!=\!\textit{eval}(\textit{app}(e_f\,e_a),\ \rho),$ $\_\!=\,\Downarrow\!(\textit{eval}(e_f,\rho),$ $\textit{clo}(\lambda(x,e_b),\ \rho_\lambda)),$ $\_\!=\,\Downarrow\!(\textit{eval}(e_a,\rho),\ v_a)$