{'fraction_non_alphanumeric': 0.02997275204359673, 'fraction_numerical': 0.007266121707538601, 'mean_word_length': 4.989130434782608, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Tractable Logic of Types

Numerous approaches to managing sort hierarchies have been proposed. Some are tractable but have limited expressive power (e.g. encoding sorts as bit strings [Fall, 1990]), others have considerable expressive power but are potentially very complex (e.g. description logics [Baader and Sattler, 2001]). The current paper proposes a logic of sorts which allows reasoning over semi-partitioned type lattices, so is more expressive than simple type hierarchies; but whose worst case complexity is linear in the size of the query, and hence is in general more tractable than description logic. The key step in implementing this logic is that we represent sorts as paths through a lattice: in the simplest case, checking that two sorts are compatible simply involves checking that the paths that make them up unify. Managing negation is rather trickier, and requires us to plant constraints that are invoked when, and only when, the relevant paths are checked. This makes the algorithm more awkward, but does not increase the (theoretical or practical) complexity of the process.