PaperlayerView exact revision on arXiv

Source-linked AI summary

Automatic Theorem Proving in Walnut

Hamoon Mousavi

arXiv:1603.06017v2cs.FLcs.LOcs.MSmath.CO

TL;DR

Deciding combinatorial properties of automatic words requires representing predicates in a form that can be handled mechanically, including across number systems. Walnut builds automata for such predicates, and its worked Thue–Morse example characterizes square orders by their binary representations.

  • Problem

    Walnut addresses mechanical decision of certain combinatorial properties of automatic words, with number representations extending beyond binary as a relevant setting.

    Source: §2.2 · p. 4, §4 · p. 12

  • Method

    Walnut builds automata for predicates from automata for subpredicates, using cross products for binary logical operators and constructions for quantification.

    Source: §4 · p. 12

  • Results

    The Thue–Morse word’s square orders have binary representations of form 0*(1|11)0*.

    Source: §7.1 · p. 24

  • Takeaways & Limitations

    Walnut’s worked example uses an automaton to characterize a combinatorial property of the Thue–Morse word.

    Source: §7.1 · p. 24

    Quantification may be theoretically inaccurate when the other number systems mix most-significant-digit and least-significant-digit conventions, so users must be cautious in such cases and for non-arithmetic quantified automata.

    Source: §4.2 · p. 15

Abstract

from arXiv · show

Walnut is a software package that implements a mechanical decision procedure for deciding certain combinatorial properties of some special words referred to as automatic words or automatic sequences. Walnut is written in Java and is open source. It is licensed under GNU General Public License.

1 Introduction

The article introduces Walnut and explains its core features, moving from basic concepts to syntax, implementation, and a user guide. It presents the tool’s capabilities through definitions and constructions tailored to Walnut rather than the most general theory.

1 Introduction

  • The article situates Walnut among work on automatic words and decision procedures, and notes prior software and applications.It points readers to related work. Walnut is open-source Java software licensed under the GNU General Public License; its minimization algorithm is based on Valmari’s algorithm [6], translated from C++ [5].Source: §1 · p. 2
  • Predicate syntax extends Presburger arithmetic with detailed semantic rules for calling and indexing automatic words.The article does not explain the already well-known semantics of Presburger arithmetic.Source: §1 · p. 2
  • Walnut constructs automata for complex predicates from simpler ones, using cross products for binary logical operators and constructions for quantification, complement, and reverse.The article also covers two less common but important automata types.Source: §1 · p. 2
  • The guide covers Walnut installation and commands, and shows how to define automata in text files and create number systems.The commands include exit, eval, def, reg, and load.Source: §1 · p. 2
  • Walnut’s notation and definitions stay close to the software’s capabilities, helping readers move from theory to application.The article uses & and A for conjunction and universal quantification, respectively.Source: §1 · p. 2

2 Basics

This section introduces Walnut’s representations of words and number systems, and explains how output automata generate automatic words while automata encode predicates about them. It also describes equal-length representations, the role of number-system annotations and variable order, and Walnut’s naming and indexing conventions.

2.1 Words and Automata

  • Walnut automata read synchronized tuples of equal-length words and accept relations; automata with output assign an output symbol to each final state.The article uses relation or tuple terminology because it describes the represented inputs more directly than the corresponding language of words.Source: §2.1 · pp. 3–4

2.2 Number Systems

  • A number system specifies an alphabet, valid representations, and a decoding to natural numbers; Walnut requires automata for representations, addition, equality, and less-than.Walnut further requires equality to coincide with word equality, and restricts number-system alphabets to finite subsets of integers.Source: §2.2 · pp. 4, 6

2.3 Automatic Words

  • An automatic word is generated by an output automaton that maps a representation of each index to the symbol at that position, enabling Walnut to decide properties such as whether it contains a square.For the Thue–Morse example, Walnut constructs automata for predicate subexpressions, applies quantifiers, and tests whether the resulting automaton accepts anything.Source: §2.3 · pp. 6–7

2.4 Automata accepting Predicates

  • For a predicate and assigned number systems for its free variables, Walnut has an automaton accepting exactly the same-length representations whose decoded values satisfy the predicate.The section states existence for predicates in Presburger arithmetic and, pending the later proof, for its extension with indexing into automatic words.Source: §2.4 · pp. 7–8
  • Annotating a predicate with number systems and fixing the free-variable order identifies a unique minimized accepting automaton; unannotated predicates default to msd_2.Annotations apply through the nearest closing parenthesis or bracket when scoped inside one, or to the predicate's end otherwise; conflicting systems for one variable or operator operands are disallowed.Source: §2.4 · p. 8
  • Walnut names for variables, words, and automata start with a letter and may contain alphanumerics and underscores; ? prefixes number-system annotations in predicates.Square brackets appear only in indexing expressions.Source: §2.4 · p. 8
  • An automaton accepts all equal-length representations of values satisfying its predicate; the a = 4 and b = 13 example omits a length-3 representation because 13 has none in msd_2.The omission is consistent with the definition of acceptance.Source: §2.4 · pp. 8–9, Figure 2.8 · p. 8
  • The example a = 1 & (?lsd_2 b = 1) shows a predicate whose variables use different number systems.The example is represented by the automaton in Figure 2.9.Source: §2.4 · p. 9, Figure 2.9 · p. 9

3 Syntax and Semantic of Predicates in Walnut

Walnut’s predicate syntax distinguishes integer-valued word alphabets, arithmetic constants, and alphabetic constants. It also restricts variable names and what may be compared with indexing expressions.

3.1 Alphabets

  • Walnut treats automatic-word symbols as integers, so W[i] can be assumed to be an integer.Source: §3.1 · p. 9

3.2 Arithmetic and Alphabetic Constants

  • Arithmetic constants must be natural numbers, while alphabetic constants use an @ prefix to refer to word symbols at positions.Source: §3.2 · p. 9
  • Alphabetic constants can be ordered like integers but cannot appear in arithmetic expressions; indexing expressions may be compared only with alphabetic constants or other indexing expressions.Source: §3.2 · p. 9

3.3 Variables

  • Variable names begin with a letter, may contain alphanumerics and underscores, and cannot be E or A.Source: §3.3 · p. 9

3.4 Operators

Walnut’s operators follow precedence and associativity rules, with parentheses available to override precedence. The article uses programming-language-style notation for logic operators.

3.4 Operators

  • A lower precedence number means higher precedence, and multiplication by a constant has the highest precedence.Source: §3.4 · p. 9
  • Parentheses override operator precedence.Source: §3.4 · p. 9
  • Operators associate left to right except complement, reverse, quantifiers, calling, and indexing, which associate right to left.Source: §3.4 · p. 9
  • Walnut uses & and A for conjunction and universal quantification to make its notation resemble programming languages.Source: §3.4 · p. 9

3.5 Arithmetic Expressions

Walnut defines arithmetic expressions recursively using natural-number constants, variables, parentheses, and restricted arithmetic operations. Such expressions are not predicates and are not accepted by automata on their own.

3.5 Arithmetic Expressions

  • Arithmetic expressions include constants, variables, and parenthesized expressions, with addition and subtraction combining arithmetic expressions.Source: §3.5 · p. 10
  • A constant expression evaluates to a natural number, so examples include 7−4 but not −1.Source: §3.5 · p. 10
  • Multiplication and division are permitted with a variable or arithmetic expression and a constant expression.Source: §3.5 · p. 10
  • An arithmetic expression alone is not a predicate, and Walnut reports an error if asked to construct an automaton for one.Source: §3.5 · p. 10

3.6 Indexing Expressions and Their Semantic Rules

Indexing expressions use arithmetic expressions or single-free-variable predicates to select positions in an automatic word. Their semantic rule evaluates the indices and checks the resulting word symbol against an alphabetic constant.

3.6 Indexing Expressions and Their Semantic Rules

  • For an n-dimensional automatic word, an indexing expression has n indices, each an arithmetic expression or a predicate with one free variable.Source: §3.6 · p. 11
  • An indexing expression alone is not a valid predicate, and automata do not accept indexing expressions by themselves.Source: §3.6 · p. 11
  • Under the indexing rule, arithmetic indices are evaluated at assigned variable values, while predicate indices must be satisfied and yield their free-variable value.Source: §3.6 · p. 11
  • The predicate W[e1]...[en] = @α holds when the word symbol at the resulting indices equals α.Source: §3.6 · p. 11
  • The same semantic approach extends to comparisons with other alphabetic constants and between indexed automatic words.Source: §3.6 · p. 11

3.7 Calling Expressions and Their Semantic Rules

A calling expression applies an automaton to arithmetic expressions or one-free-variable predicates, and its semantics evaluate those arguments before testing the automaton’s predicate.

3.7 Calling Expressions and Their Semantic Rules

  • A calling expression has the form $M(e1,e2,...,en), where each argument is an arithmetic expression or a predicate with one free variable, and is itself a valid predicate.Here M is an automaton with n inputs.Source: §3.7 · p. 11
  • The call is satisfied when the automaton’s predicate P holds after each input variable yi is assigned its corresponding argument value ai.The semantic rule evaluates the arguments first, then checks P with those values.Source: §3.7 · p. 11
  • For arithmetic arguments, the corresponding value ai is the expression’s value under the given substitutions; for predicate arguments, the predicate must hold and ai is the value of its free variable.Source: §3.7 · p. 11

3.8 Relative Expressions

Relative expressions include comparisons between arithmetic expressions, between indexing expressions or alphabetic constants, and calling expressions; each is a predicate.

3.8 Relative Expressions

  • A comparison between two arithmetic expressions is a relative expression, using any of =, !=, <, >, <=, or >=.Source: §3.8 · p. 11
  • A comparison between indexing expressions and/or alphabetic constants is also a relative expression.Source: §3.8 · p. 11
  • A calling expression is relative, but a mixed comparison such as W[a] = b + 2 is not; every relative expression is a predicate.The example mixes an indexing expression with an arithmetic expression.Source: §3.8 · p. 11

3.9 Predicates

Predicates are built from relative expressions using logical operators and quantifiers, with their truth conditions extending first-order logic and Presburger arithmetic through indexing and calling.

3.9 Predicates

  • Every relative expression is a predicate, and predicates remain predicates under parentheses, negation, and logical combination.Source: §3.9 · p. 12
  • Existential and universal quantification over free variables also form predicates.Source: §3.9 · p. 12
  • Predicate semantics add the rules for indexing and calling to the familiar semantics of first-order logic and Presburger arithmetic; Walnut’s eval and def commands convert predicates to automata.Source: §3.9 · p. 12

4 Decision Procedure: Walnut’s Implementation

This section describes how Walnut implements its decision procedure by constructing complex predicate automata from basic automata and reusing them through argument substitutions. It also covers output automata for indexing and comparing automatic words, command behavior, and an argument-number-system requirement.

4 Decision Procedure: Walnut’s Implementation

  • Walnut's decision procedure constructs automata for complex predicates from the basic automata it knows for each defined number system.The procedure covers binary logical operators, existential and universal quantification, complement, reverse, and arithmetic and comparison expressions.Source: §4 · p. 12

4.1 Cross Product

  • Walnut constructs automata for conjunction by taking a cross product, selecting appropriate final states, and minimizing; related final-state choices handle other binary logical operators.The construction requires shared variables in both predicates to have consistent number-system annotations.Source: §4.1 · pp. 12–13

4.2 Quantification

  • For existential quantification, Walnut removes the quantified coordinate, restores tuples differing only by leading or trailing zeros, then determinizes and minimizes.For mixed msd and lsd systems, or non-arithmetic quantified automata, Walnut only constructs the coordinate-eliminated automaton, which is not theoretically accurate.Source: §4.2 · pp. 14–15

4.3 Complement and Reverse

  • Walnut complements an automaton by totalizing it, swapping final and non-final states, and intersecting with the valid-representation automaton; reverse reverses all transitions.Universal quantification is obtained as the complement of existential quantification applied to the complemented predicate.Source: §4.3 · pp. 15–16, §4.2 · p. 15

4.4 Arithmetic and Comparison Operators

  • Walnut derives arithmetic and comparison automata from addition, equality, and less-than automata, recursively handling constants and expressing compound arithmetic with existentially quantified intermediate results.Because arithmetic is over natural numbers, subtraction or division placed before later operations can exclude otherwise intended cases; the paper recommends postponing them to the rightmost position.Source: §4.4 · pp. 16–17

4.5 Calling an Automaton

  • A calling expression lets a predicate reuse a previously computed, named automaton by supplying arguments for its variables.The syntax is $M(e1,e2,...,en), where each argument is an arithmetic expression or a predicate with exactly one free variable.Source: §4.5 · pp. 17–18
  • Walnut calls a predicate’s automaton by forming an equivalent predicate through argument substitutions; variables need no fresh variable, improving construction efficiency.Calling the automaton avoids copying its predicate repeatedly and reconstructing the automaton at each occurrence.Source: §4.5 · p. 18
  • The eval command constructs an automaton from a predicate, while def also saves it for later calls from other predicates.The text directs readers to Section 7.2 for more examples of def.Source: §4.5 · p. 18
  • Each argument supplied when calling an automaton must use the same number system as the corresponding input.Source: §4.5 · p. 18

4.6 Indexing an Automatic Word

  • For indexing an automatic word, Walnut uses its corresponding automaton with output; constructions involving arithmetic-expression indices or one-free-variable predicates use substitutions.Source: §4.6 · p. 18
  • The equality relation between two indexed automatic words is represented by the minimized product automaton whose state pairs have the same output.The text says analogous constructions apply to other comparison operators.Source: §4.6 · p. 18

5 Special Automata in Walnut

Walnut uses special true and false automata for predicates that evaluate to those values, with conventions for simplifying logical operations. Non-arithmetic automata let inputs represent patterns or non-numeric instructions rather than numbers in a particular number system.

5.1 True and False Automata

  • Predicates without free variables that evaluate true or false receive the corresponding special automaton; predicates with free variables can also become true or false automata.For example, Walnut treats a predicate with an impossible existential condition as false and its negation as true.Source: §5.1 · p. 19
  • Walnut’s conventions make conjunction or disjunction with true and false automata follow the corresponding logical identities, and negation swaps the two automata.Other logical-operator conventions follow from these rules.Source: §5.1 · p. 19

5.2 Non-arithmetic Automata

  • Non-arithmetic automata accept patterns or use non-numeric instructions, allowing the same pattern automaton to be called in both msd_2 and lsd_2 predicates.For paperfolding words, one input represents a position and another represents a folding instruction; see.Source: §5.2 · p. 19

6 Installation

Walnut can be run from the command line on a system with Java 8 or later. The article also describes running it in Eclipse and explains requirements for viewing automaton drawings and handling text files.

6 Installation

  • Walnut runs from the command line on any platform with Java 8 or later; the installation instructions begin by uncompressing the archive and launching the program from its bin directory.The article also gives a command for exiting Walnut.Source: §6 · p. 20
  • Viewing Walnut’s .gv automaton drawings requires Graphviz, and text files read or produced by Walnut use UTF-8 encoding.The passage notes that most text editors use UTF-8 by default.Source: §6 · p. 20

6.1 Eclipse

  • In Eclipse, import Walnut as an existing project, open prover.java, run it, and enter Walnut commands in the IDE console.The article recommends using an IDE console as a more convenient alternative to the terminal.Source: §6.1 · p. 20

7 Commands

Section 7 describes Walnut commands for evaluating predicates into automata and saving, defining, reusing, and expanding automata and predicate templates. It also covers incidence matrices, regular-expression-based automata construction, command files, and examples across number systems and words, including squares and overlaps in the Thue–Morse word.

7 Commands

  • A single colon reports major computation steps, a double colon exposes intermediate operations, and a semicolon suppresses those reports; Walnut also ignores whitespace and reports command errors.The listed command forms include eval, macro, and reg with either a number system or an alphabet.Source: §7 · pp. 20–22

7.1 eval: eval <name> <predicate>

  • Walnut’s eval command takes an evaluation name and a quoted predicate; resulting files share that name, and the example automaton is saved as four.gv; Walnut defaults to msd_2.Source: §7.1 · p. 22

7.2 def: def <name> <predicate>

  • Automata created with def are saved in the Automata Library and can be called later using $, with arguments that may be variables, constants, arithmetic expressions, or predicates.The examples also show that a function argument cannot be an automaton with other than one input.Source: §7.2 · pp. 26–27
  • The def examples show that input roles matter: applying f1 to (a,1) accepts numbers greater than 1, while f2 accepts numbers less than 1.Walnut orders automaton inputs by the lexicographic order of their labels, and the number of supplied arguments must match the automaton’s inputs.Source: §7.2 · p. 27

7.3 macro: macro <name> <template>

  • Macros store predicate templates for reuse across words, whereas def stores the automaton calculated for a predicate; Walnut does not accept nested macro or function calls.Before eval and def, Walnut replaces macros with their templates and substitutes the supplied arguments.Source: §7.3 · p. 28

7.4 Matrices with eval and def

  • Optional free-variable lists make eval and def calculate and save incidence matrices for automaton transitions labeled by those variables.Each matrix entry counts transitions between a pair of states whose label tuple has the specified value in that variable’s coordinate; matrices are saved in Maple syntax in /Walnut/Result/.Source: §7.4 · p. 29

7.5 reg

  • The reg command constructs automata from regular expressions, either for a specified number system or for an alphabet, enabling non-arithmetic automata usable with different number systems.The alphabet-based form is limited to subsets of {0,1,...,9}, and Walnut requires matching input alphabets when combining automata; the text identifies this strictness as a drawback.Source: §7.5 · pp. 30–31

7.6 load: load <file name>

  • The load command runs all legitimate Walnut commands in a text file, in their listed order, and the file must use UTF-8 encoding.Command files are saved in the /Walnut/Command Files/ directory.Source: §7.6 · p. 31

8 Working with Input/Output

The input/output guide describes Walnut’s text-file conventions for automata, automatic words, and custom number systems, alongside a UTF-8 assumption and instructions for converting automaton drawings.

8 Working with Input/Output

  • The input/output instructions assume that all files use UTF-8 encoding.Source: §8 · p. 32

8.1 Defining Automata in Text Files

  • Automaton text files declare input number systems, states, and transitions; undeclared transitions lead to a dead state, wildcard symbols can match inputs, and the output alphabet is inferred from state declarations.The stated file format declares state 0 after the first line and proceeds through the remaining states and their transitions.Source: §8.1 · p. 32
  • Non-arithmetic automata declare explicit alphabets for inputs without number systems, while true and false automata each take a one-line text-file definition.The section also introduces an automaton for paperfolding words.Source: §8.1 · p. 32

8.2 Defining New Automatic Words

  • Defining a new automatic word requires manually defining its automaton with output in Walnut’s Word Automata Library, because eval and def produce predicate automata instead.The Thue-Morse word is given as an example.Source: §8.2 · p. 33

8.3 Defining New Number Systems

  • A custom number system requires automata for representations, addition, and less-than; an equality automaton can be generated from equal-length identical words.The corresponding files go in Custom Bases, with filenames depending on whether the system is msd or lsd.Source: §8.3 · p. 33
  • Walnut can derive lsd automata by reversing msd automata for msd_n and msd_fib, but the article cautions that other systems may differ in more than transition direction.Source: §8.3 · p. 34

8.4 Converting .gv files to .jpeg

  • Graphviz can open Walnut’s .gv drawings and convert them to other formats, including JPEG.Source: §8.4 · p. 34
Loading 1603.06017v2…