Relational conditionals with pseudo-functions
Vo, Khoa (2019)
Julkaisun pysyvä osoite on
https://urn.fi/URN:NBN:fi:amk-2019051710424
https://urn.fi/URN:NBN:fi:amk-2019051710424
Tiivistelmä
Relational programming promises the ability to run programs backwards. Using miniKanren, it is easy to convert pure functions into relations. And because of its embedded nature, programmers can enjoy the declarative power of miniKanren without leaving the comfort of their favorite programming languages. Even though this thesis chooses to discuss the Scheme implementation of the language, the techniques presented here is general for all implementations.
Some miniKanren users prefer to first write a prototype in a functional manner in Scheme, and later transform that prototype into its relational counterpart. Despite being an easy task, this transformation frequently increases the code size. As programs grow longer, there are more chances for human errors to creep in.
One reason for this size increase (and why some people want to write programs functionally in the first place) has to do with the symbiosis between Boolean-returning functions and conditionals. Branching has long been a powerful programming tool, yet they have no adequate counterpart in miniKanren. conda and condu cannot be used relationally as they are logically impure. And even though new users are guided to convert all cond expressions to conde, conde clauses do not automatically deny preceding tests, a job which is then delegated to the one performing the conversion. As a result, many programs lose their compactness and structural clarity after the conversion.
This thesis aims to provide frameworks and techniques for writing conditionals in miniKanren as well as a way to analyze the correctness of pre-existing miniKanren programs using conditionals. As for the former, the goal constructor condo along with test combinators conjt and disjt are introduced. Concerning the latter, a more involved method of static analysis and rewriting is used, resulting in a new language variant called staticKanren.
Some miniKanren users prefer to first write a prototype in a functional manner in Scheme, and later transform that prototype into its relational counterpart. Despite being an easy task, this transformation frequently increases the code size. As programs grow longer, there are more chances for human errors to creep in.
One reason for this size increase (and why some people want to write programs functionally in the first place) has to do with the symbiosis between Boolean-returning functions and conditionals. Branching has long been a powerful programming tool, yet they have no adequate counterpart in miniKanren. conda and condu cannot be used relationally as they are logically impure. And even though new users are guided to convert all cond expressions to conde, conde clauses do not automatically deny preceding tests, a job which is then delegated to the one performing the conversion. As a result, many programs lose their compactness and structural clarity after the conversion.
This thesis aims to provide frameworks and techniques for writing conditionals in miniKanren as well as a way to analyze the correctness of pre-existing miniKanren programs using conditionals. As for the former, the goal constructor condo along with test combinators conjt and disjt are introduced. Concerning the latter, a more involved method of static analysis and rewriting is used, resulting in a new language variant called staticKanren.