Products, Polynomials and Differential Equations in the Stream Calculus

被引:0
作者
Boreale, Michele [1 ]
Collodi, Luisa [1 ]
Gorla, Daniele [2 ]
机构
[1] Univ Firenze, Dipartimento Stat Informat Applicaz G Parent, Viale Morgagni,65, I-50134 Florence, Italy
[2] Univ Roma La Sapienza, Dipartimento Informat, Viale Regina Elena,295, I-00161 Rome, Italy
关键词
Streams; polynomials; differential equations; coalgebra; algebraic geometry;
D O I
10.1145/3632747
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We study connections among polynomials, differential equations, and streams over a field K, in terms of algebra and coalgebra. We first introduce the class of (F, G)-products on streams, those where the stream derivative of a product can be expressed as a polynomial function of the streams and their derivatives. Our first result is that, for every (F, G)-product, there is a canonical way to construct a transition function on polynomials such that the resulting unique final coalgebra morphism from polynomials into streams is the (unique) commutative K-algebra homomorphism-and vice versa. This implies that one can algebraically reason on streams via their polynomial representation. We apply this result to obtain an algebraic-geometric decision algorithm for polynomial stream equivalence, for an underlying generic (F, G)-product. Finally, we extend this algorithm to solve a more general problem: finding all valid polynomial equalities that fit in a user specified polynomial template.
引用
收藏
页数:25
相关论文
共 31 条
[1]  
[Anonymous], 2002, NONLINEAR SYSTEMS
[2]  
Basold Henning, 2014, Horizons of the Mind. A Tribute to Prakash Panangaden. Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday: LNCS 8464, P124, DOI 10.1007/978-3-319-06880-0_6
[3]   Newton series, coinductively: a comparative study of composition [J].
Basold, Henning ;
Hansen, Helle Hvid ;
Pin, Jean-Eric ;
Rutten, Jan .
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2019, 29 (01) :38-66
[4]  
Bhaduri Purandar, 2023, Log. Methods Comput. Sci, V19, P38
[5]   Coinduction Up-To in a Fibrational Setting [J].
Bonchi, Filippo ;
Petrisan, Daniela ;
Pous, Damien ;
Rot, Jurriaan .
PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2014,
[6]   A coalgebraic perspective on linear weighted automata [J].
Bonchi, Filippo ;
Bonsangue, Marcello ;
Boreale, Michele ;
Rutten, Jan ;
Silva, Alexandra .
INFORMATION AND COMPUTATION, 2012, 211 :77-105
[7]   PRESENTING DISTRIBUTIVE LAWS [J].
Bonsangue, Marcello M. ;
Hansen, Helle H. ;
Kurz, Alexander ;
Rot, Jurriaan .
LOGICAL METHODS IN COMPUTER SCIENCE, 2015, 11 (03)
[8]   Automatic Pre- and Postconditions for Partial Differential Equations [J].
Boreale, Michele .
QUANTITATIVE EVALUATION OF SYSTEMS (QEST 2020), 2020, 12289 :193-210
[9]   Complete algorithms for algebraic strongest postconditions and weakest preconditions in polynomial ODES [J].
Boreale, Michele .
SCIENCE OF COMPUTER PROGRAMMING, 2020, 193
[10]   ALGEBRA, COALGEBRA, AND MINIMIZATION IN POLYNOMIAL DIFFERENTIAL EQUATIONS [J].
Boreale, Michele .
LOGICAL METHODS IN COMPUTER SCIENCE, 2019, 15 (01) :14:1-14:27