[madPL] Synthesis / SemGuS Reading Group

[EVAN XINGYE GENG <egeng@xxxxxxxx>]

Hello, PL fans!

 

We are once again hosting the weekly Synthesis / SemGuS Reading Group, and you are invited to join us on Thursdays from 1 to 2 on Zoom:

https://uwmadison.zoom.us/j/96450343227?pwd=emtGcHROSVZoOWsyWEFhN2wyazA2Zz09

 

This week, I am going to be presenting the "miniKanren" relational logic programming system (in particular, some of the implementation details and results from Relational Programming in miniKanren: Techniques, Applications, and Implementations (W. Byrd, 2009)).

 

Abstract:

The promise of logic programming is that programs can be written relationally, without distinguishing between input and output arguments. Relational programs are remarkably flexibleâfor example, a relational type-inferencer also performs type checking and type inhabitation, while a relational theorem prover generates theorems as well as proofs and can even be used as a simple proof assistant. Unfortunately, writing relational programs is difficult, and requires many interesting and unusual tools and techniquesâ In this dissertation I present miniKanren, a family of languages specifically designed for relational programming, and which supports a variety of relational idioms and techniques. I show how miniKanren can be used to write interesting relational programsâ [and] also present interesting and practical techniques used to implement miniKanren, including a nominal unifier that uses triangular rather than idempotent substitutions and a novel âwalkâ-based algorithm for variable lookup in triangular substitutions. The result of this research is a family of languages that supports a variety of relational idioms and techniques, making it feasible and useful to write interesting programs as relations.

 

âHomework Questionâ:

It is often useful to express âclassicalâ functions as relations relating inputs to outputs. For instance, the Boolean function and: (Bool, Bool) -> Bool might be expressed as a relation and^o: (Bool à Bool) à Bool, where and^o((a, b), c) holds when c = a â b. In miniKanren, relations such as and^o can be constructed explicitly using a small set of operatorsânamely: the existential quantifier â, logical conjunction â, logical disjunction â, equality/unification =, and the list/pair construction function cons. We could write the and^o relation in this way as:

 

             and^o((a, b), c) â (c=1 â a=1 â b=1) â (c=0 â (a=0 â b=0))

 

To illustrate the other operators, we might write a relation for the empty? function, which checks if a list is empty or not, as follows:

 

             empty^o(x, r) â (r=1 â x=[]) â (r=0 â (âh, t. x=(cons h t)))

 

Equipped with these tools, can you encode more complex functions as relationsâ say, arithmetic on the naturals? HINT: To do this, youâll first have to think about how you can encode numbers using the provided operators.

 

Thanks,

- Evan Geng

 

(Sometimes, I wish I could typeset my emails in LaTeX)