2023/02/05 by Ezra e. k. Cooper, Cooper, Ezra e. k.
Computer Science · #Computability, Logic, AI Algorithms #F.4.2 #FOS: Computer and information sciences #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2302.02462
openalex publication_date 2023/02/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In the research on computational effects, defined algebraically, effect symbols are often expected to obey certain equations. If we orient these equations, we get a rewrite system, which may be an effective way of transforming or optimizing the effects in a program. In order to do so, we need to establish strong normalization, or termination, of the rewrite system. Here we define a framework for carrying out such proofs, and extend the well-known Recursive Path Ordering of Dershowitz to show termination of some effect systems.