| 研究実績の概要 |
As planned, I have been working on the problem of performing global optimizations on DSLs embedded in the tagless-final style. I have developed the approach of using normalization-by-evaluation~-- rather than term re-writing~-- to transform a program to the normal form. The approach has proved successful. First, I was able to reproduce, in a much simpler way, the previous work in optimizing language-integrated database queries and compiling them to SQL. Mainly, the approach was readily extended to queries that involved ordering and subranging operations. For the first time we have proposed the compositional semantics of these query operations. The developed language-integrated query system is the first that supports ordering and subranging in a portable and consistent way. The results have been published.
I have applied the tagless-final DSL approach to the completely different domain: transforming terms representing natural language sentences into logical formulas. This work is a part of a large project on natural language comprehension. Although it is just the beginning, I have already reported successful results on the first part (generalized quantifiers) of the FraCAS textual entailment corpus. The corresponding paper has been accepted for publication.
There are more applications of the denotational/tagless-final approach, described in further submitted papers.
|
| 今後の研究の推進方策 |
In the FY2018, I will work on further applications of the developed approach, to demonstrate its expressive power and that the achieved results are not a fluke. First, I will implement a DSL for generating highest-performance numerical kernels for the general-purpose GPU (GPGPU) programming. The target language is OpenCL. The goal is to reproduce, and hopefully, exceed the performance of the state-of-the-art ``lift'' GPGPU framework, but in a type-safe way. To achieve the highest performance, the DSL should be able to express the GPU memory hierarchy.
Another application is the framework for reasoning about tagless-final DSLs. I will investigate abstract interpretation, and denotational semantics of DSL programs with computational effects such as mutation and non-determinism.
|
