L10 Language Specification

This document gives a specification of the grammar of L10 programs and talks a little bit about their meaning; some example L10 programs can be found on the examples page.

This document is incomplete

Syntax

Lexical conventions

Single-line comments take the form "// ... \n".

Lower-case identifiers are any sequence of alphanumeric characters that start with a lower-case identifiers (a-z). Upper-case identifiers are any sequence of alphanumeric characters, underscores, and single quotes (') that start with a capital letter (A-Z). A string of numeric characters (0-9) is a natural number literal, and the quote character ("), followed by a series of alphanumeric characters, underscores, single quotes, and spaces and terminated by another quote character is a string literal.

Reserved identifiers are:

Negation not and existential quantification Ex.
Built-in types and kinds t, nat, string, world, type, and rel.

An underscore is treated as a special upper-case identifier that we do not care about.

Terms and atomic propositions

Terms and atomic propositions are both formed from the same very basic grammar; the only interesting special case is addition, which computes the addition of two known natural numbers.

UCID ::= (upper-case identifiers) | _
ID ::= (lower-case identifiers) | (natural number literals) | (string literals) 
TERM ::= UCID | ID | TERM TERM | TERM + TERM

Propositions and rules

Premises and conclusions are basically a series of atomic propositions, though some premises may be negated or be the special comparison propositions. Equality and equality are valid on terms of any type, but inequality can only be used on terms of the nat type of natural numbers.

ATOM  ::= ID | ATOM TERM
ATOMS ::= ATOM | ATOM, ATOMS
PAT   ::= ATOM | Ex ID. PREM 
PREM  ::= PAT | not PAT         
        | TERM == TERM | TERM != TERM 
        | TERM < TERM | TERM <= TERM  
        | TERM => TERM | TERM > TERM  
PREMS ::= PREM | PREM, PREMS
RULE  ::= PREMS | PREMS -> ATOMS

Classifiers, declarations, and the signature

ATYPE ::= t | nat | string | LCID          // Atomic types

TYPE  ::= ATYPE                            // Constant type 
        | ATYPE -> TYPE                    // Constructor type
        | {LCID : ATYPE} TYPE              // Named constructor type

KIND  ::= ATYPE -> KIND                    // Argument
        | {LCID : ATYPE} KIND              // Named argument
        | type                             // Type
        | world                            // World
        | rel @ ATOM                       // Forward-chaining proposition

DECL  ::= LCID : TYPE.                     // New constant of a given type
        | LCID : KIND.                     // New world/type/proposition
        | RULE.                            // New rule
        | LCID = PROPS @ WORLD.            // Perform a computation

SIG   ::=                                  // Empty signature 
        | DECL SIG                         // Declaration

There is also a backwards-facing arrow <- that is syntatic sugar for a forward-facing arrow with the front and back switched.

Precedence

Application binds more tightly than anything else.

binds least tightly ---> =   :
                         <- (left associative)
                         -> (right associative)
                         , (left associative)
                         @ 
                         ==   !=   >   <   >=   <= 
                         + (left associative)
binds most tightly --->  (application)

Well-formed programs

Well-typed terms

(Talk about the behavior of the default type t.)

Well-formed declarations

(Declarations of new propositions must be well-scoped, and ordering declarations w1 < w2 can't cause cycles.)

L10 Logic Programming Language