An Emptiness Algorithm for Regular Types with Set Operators

TL;DR

This paper introduces an algorithm that determines the emptiness, equivalence, and inclusion of regular type expressions with set operators, generalizing previous methods by removing tuple distributivity assumptions.

Contribution

The paper presents a novel algorithm capable of handling regular type expressions with set operators without assuming tuple distributivity, enabling broader applicability.

Findings

Algorithm effectively decides emptiness, equivalence, and inclusion of complex type expressions.

Generalizes previous algorithms by allowing set operators in type expressions.

Provides a more flexible approach to regular type analysis.

Abstract

An algorithm to decide the emptiness of a regular type expression with set operators given a set of parameterised type definitions is presented. The algorithm can also be used to decide the equivalence of two regular type expressions and the inclusion of one regular type expression in another. The algorithm strictly generalises previous work in that tuple distributivity is not assumed and set operators are permitted in type expressions.