A Specification's Realm: Characterizing the Knowledge Required for Executing a Given Algorithm Specification

TL;DR

This paper introduces the concept of an 'algorithm specification's realm,' a comprehensive knowledge document needed for executing an algorithm independently, and discusses how to systematically generate and utilize it for verification and implementation.

Contribution

It proposes a formal characterization of the knowledge required for executing algorithm specifications and suggests automated methods for generating this knowledge using language models.

Findings

The realm includes syntax, semantics, domain knowledge, and operational instructions.

Systematic generation of the realm can be partially automated with language models.

Characterizing the realm aids in implementation and formal verification of algorithms.

Abstract

An algorithm specification in natural language or pseudocode is expected to be clear and explicit enough to enable mechanical execution. In this position paper we contribute an initial characterization of the knowledge that an executing agent, human or machine, should possess in order to be able to carry out the instructions of a given algorithm specification as a stand-alone entity, independent of any system implementation. We argue that, for that algorithm specification, such prerequisite knowledge, whether unique or shared with other specifications, can be summarized in a document of practical size. We term this document the realm of the algorithm specification. The generation of such a realm is itself a systematic analytical process, significant parts of which can be automated with the help of large language models and the reuse of existing documents. The algorithm-specification's realm would consist of specification language syntax and semantics, domain knowledge restricted to the referenced entities, inter-entity relationships, relevant underlying cause-and-effect rules, and detailed instructions and means for carrying out certain operations. Such characterization of the realm can contribute to methodological implementation of the algorithm specification in diverse systems and to its formalization for mechanical verification. The paper also touches upon the question of assessing execution faithfulness, which is distinct from correctness: in the absence of a reference interpretation of natural language or pseudocode specification with a given vocabulary, how can we determine if an observed agent's execution indeed complies with the input specification.