In this paper, we formalize practical byte pair encoding tokenization as it is used in large language models and other NLP systems. There are subtle differences between implementations, so we in particular formally define and investigate the semantics of the SentencePiece and HuggingFace tokenizers, and how they relate to each other. These differences depend on the details of how the dictionary of tokenization rules is constructed. Beyond this, we consider how tokenization can be performed in an incremental fashion, as well as doing it left-to-right using an amount of memory constant in the length of the string, enabling e.g. using a finite state string-to-string transducer.