Rewriting preserving recognizability of finite tree languages

We show that left-linear generalized semi-monadic TRSs effectively preserve recognizability of finite tree languages (are EPRF-TRSs). We show that reachability, joinability, and local confluence are decidable for EPRF-TRSs.

► The concept of an EPRF-TRS is introduced.
► An EPRF-TRS effectively preserves recognizability of finite tree languages.
► We show that left-linear generalized semi-monadic TRSs are EPRF-TRSs.
► We show that each terminating TRS is an EPRF-TRS.
► We show that reachability, joinability, local confluence are decidable for EPRF-TRSs.