DOCUMENTATION

EXPRESSION LANGUAGE

QBAR uses an s-expression language to describe all of its data structures and abstract syntax. S-expressions are parenthesis-grouped strings which can be distinguished into two basic forms: atoms and groups. S-expressions are the syntax of choice for LISP dialects like Common Lisp, Clojure, Racket, and many others. QBAR expressions are slightly more general in that they intend to describe arbitrary data rather than just programs. See Rivest S-expressions which have a similar goal.

NOTE: Objects marked with ⚠️ have an unstable API.

Basic Forms

Expressions are either atoms, groups, or unspecified, in which case they are simply called exprs.

atom ⚠️

An atom is any Unicode string which uses " to wrap whitespace and ( ). Here are some examples:

      123

      "a b c"

      f"Hello, {world}!"

      "multi-line
      strings"

      text-before-the-quote"text in the quote"text-after-the-quote

      []{}<>-are-also"atoms since we only care about ()"<-notice_we_had_to_escape"("and")"

      emoji.too:🗿:😂
    

Here's a regular expression that parses atoms:

RAW SYNTAX
([^\"\(\s\)]+((\"[^\"]*\")[^\"\(\s\)]*)*)|([^\"\(\s\)]*((\"[^\"]*\")[^\"\(\s\)]*)+)

NOTE: Currently, only whitespace literals and parenthesis are escaped in quoted strings. In the future, other escape sequences may be supported.

group

A group is an expression formed by bracketing with an open parenthesis (, delimiting with whitespace a set of expressions and then ending with a close parenthesis ).

SYNTAX
( whitespace? {expr whitespace?}* )

expr

An expr is either an atom or a group

SYNTAX
atom | group

Important Shapes

NOTE: Shapes have the same syntax as expressions except we don't notate optional whitespace and wrapping group, and [$name: $shape] objects are used to name the shape elements.

The following are some important shapes:

substitution

A substitution represents a piecewise transformation of the kind Atom -> Expr mapped over an expressions atoms. For every var which appears in a given expression, expr replaces every occurence of that atom in the entire expression.

SHAPE
{[var: atom] [expr: expr]}*

NOTE: If two equal var appear in the same substitution, the first one is used.

• shell subst command

rule

A rule represents a stateful inference rule which can be joined with substitutions to make a composition.

SHAPE
[top: group] [bot: group]

The top expression is also known as the premise and the bot expression is also known as the conclusion.

composition

A composition represents a chain of rule-substitution pairs composed from top to bottom.

SHAPE
{[rule: {hash | rule}] [substitution: {hash | substitution}]}*

ruleset

A ruleset is a collection of rules along with a set of substitution constants which are not allowed to be substituted out of. A composition belongs to the closure of a ruleset if all of its rules are in the ruleset and no substitution has any constant as one of its var.

SHAPE
[constants: ( atom* )] [rules: ( {hash | rule}* )]

definition ⚠️

A definition is the assignment of a name and variables to an expression.

SHAPE
def [name: atom] [vars: ( atom* )] [expr: expr]

defset

This shape represents any collection of definitions. For the shape to be a valid set of definitions, it must not contain duplicate name assignments.

SHAPE
{hash | definition}*

Reference Parsers

Currently all expression parsers are built into the reference shell implementations. In the future, they will be separated into their own libraries.

SHELL

The shell is the default way to interact with QBAR expressions. You can use the shell to build, verify, and analyze compositions and other proof objects.

Commands

The following are a list of the currently implemented commands.

NOTE: Commands marked with ⚠️ have an unstable name, API, and/or signature.

clear

config ⚠️

docs ⚠️

eval ⚠️

find ⚠️

info ⚠️

load ⚠️

ruleset ⚠️

search ⚠️

subst: <expr> <substitution>

tutorial ⚠️

verify ⚠️

version

exit

Keybindings

The following are the default shell emacs-like keybindings for the reference shell implementations. Custom and vim-like keybindings are not yet implemented.

^A

^C

^D

^E

^L

Reference Implementations

The qbar toolkit comes with two reference shell implementations written in Rust:

Terminal

The reference terminal shell can be installed with cargo as follows:

cargo install qbar

For more information on the terminal shell implementation see the Rust documentation.

Web

The reference web shell is built off of the reference terminal shell and can be accessed on the main qbar website. For more information on the web shell implementation see the Rust documentation.