一句话:综述流微分方程的多种规格格式、求解方法及其可定义流类,并阐明语法解法与抽象 GSOS 的联系。
流(无限序列)类型简单却理论丰富。流微分方程是一种用余归纳方式指定流及流运算的方法,过去二十年积累了众多结果。本文对此进行综述:重点分类不同格式的流微分方程,梳理其求解方法,以及各类格式所能定义的流类;并详细讨论所谓的语法求解方法与抽象 GSOS 之间的关系。该工作为理解流规范语言的表达力、解的存在唯一性与余代数语义提供了统一视角。
Streams, or infinite sequences, are infinite objects of a very simple type, yet they have a rich theory partly due to their ubiquity in mathematics and computer science. Stream differential equations are a coinductive method for specifying streams and stream operations, and their theory has been developed in many papers over the past two decades. In this paper we present a survey of the many results in this area. Our focus is on the classification of different formats of stream differential equations, their solution methods, and the classes of streams they can define. Moreover, we describe in detail the connection between the so-called syntactic solution method and abstract GSOS.
@article{paperbot207,
title = {Stream Differential Equations: Specification Formats and Solution Methods},
author = {Helle Hvid Hansen and Clemens Kupke and Jan Rutten},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 1},
year = {2017},
doi = {10.23638/lmcs-13(1:3)2017}
}