研究実績の概要 |
As planned, in 2019 I, together with a master student, accomplished the second main project goal: using tagless-final to embed Logical-framework--like DSL for specifying typed calculi, for prototyping of functional languages and their type systems and, in particular, natural language semantic theories. We have implemented a DSL for describing derivations in AB grammars, Lambek grammars, and Kubota and Levin's Hybrid Type-Logical grammars. Not only we mechanically check that derivations are well-formed, but we also format them as LaTeX figures according to the common theoretical-linguistic conventions. That research has lead to an unexpected result in the field of Formal Grammar: an algebraic presentation of Lambek Grammars and the demonstration that under a natural restriction (satisfied in natural languages), Lambek grammars are strongly equivalent to context-free grammars, strengthening the existing solutions to this long-standing problem. As part of disseminating research results and making them more accessible and applicable, I have delivered a three-lecture course at the International Summer School on Metaprogramming, on the tagless-final approach and its algebraic semantics. I have investigated abstract interpretation, and denotational semantics of DSL programs with computational effects such as mutation and non-determinism, whose results are published in a journal paper (EPTCS 294). I have used the tagless-final approach in writing code to assist in theoretical work in lambda-calculus, whose results are published as a journal paper (J. Functional Programming, v30).
|