HashTrie Functional Framework and Its Application in Chinese-English Pattern Matching

Most existing multi-pattern matching algorithms are designed for single English texts leading to issues such as missed matches and space expansion when applied to Chinese-English mixed-text environments. The HashTrie-based matching machine demonstrates strong compatibility with both Chinese and English, ensuring high accuracy in text processing and subtree positioning. In this study, a novel functional framework based on the HashTrie structure is proposed and mechanically verified using Isabelle/HOL. This framework is applied to design Functional Multi-Pattern Matching (FMPM), the first functional multi-pattern matching algorithm for Chinese-English mixed texts. FMPM constructs the HashTrie matching machine using character codes and threads the machine according to the associations between pattern strings. The experimental results show that as the stored string information increases, the proposed algorithm demonstrates more significant optimization in retrieval efficiency. FMPM simplifies the implementation of the Threaded Hash Trie (THT) for Chinese-English mixed texts, effectively reducing the uncertainties in the transition from the algorithm description to code implementation. FMPM addresses the problem of space explosion Chinese-English mixed texts and avoids issues such as bound variable iteration errors. The functional framework of the HashTrie structure serves as a reference for the formal verification of future HashTrie-based algorithms.