Subject: Term

Keywords: ::tips

Title: ascii term syntax

--------------------------------------------------

<term>      : {<parameter list>}(<term list>)
<term list> : <term>
            | <term>; <term list>
<parameter list> : <parameter>
                 | <parameter>, <parameter list>
<parameter> : <parameter value>:<parameter type>
<parameter value> : STRING
<parameter type>  : STRING

While a <parameter type> can be any string, the following types are
used by nuprl :
 v :    variable
 s :    string
 n :    natural number
 t :    token
 o :    ObjectId
 OPID : opid

While a <parameter value> can be any string it is expected
that the string is interpretable as a member of its type.

STRING:
 The following characters must be escaped with \ in strings : \{,}(;)
 Only printable ascii characters are allowed, it is left to the user to
 encode other charaters into ascii.

Variable:
 There is no special syntax for variables beyond the variable parameter type.
 An instance of the variable v would occur as {variable:OPID, x:v}() 
Binding:
 Variable bindings are encoded as terms.
 For example λx.x is exported as
 {lambda:OPID}({bound_id:OPID,x:v}({variable:OPID,x:v}()))

OPID:
 Historically (and still internally) nuprl terms had a required
 first parameter with implicit type OPID. To be more general this
 requirement has been relaxed, but for the purposes of backward
 compatability certain oddities exists. For example, the term
 {variable:OPID, x:v}() could have been more naturally written as
 {x:v}()


Whitespace:
 Whitespace is ignored except in STRINGs, terms can be exported with
 or without whitespace. Whitespace allows breaks and indentations to 
 be used to reflect the tree structure of the term and make the output
 more readable.
  
 ⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home