mod Msyntax

incl Mtex

rem 
  \para \bf  Chapter. Syntax of CL.  \end 

rem 
  \para \bf  Section. Terms and Formulas.  \end 

rem 
  \para \bf  Variables.  \end Variable identifiers are strings of lower case 
  letters possibly followed by one or two digits as indices. 
  \para Examples: \ft x \end, \ft ys \end, \ft i1 \end, \ft foo99 \end. 

rem 
  \para \bf  Function and predicate symbols.  \end Function and predicate 
  identifiers are alpha-numeric strings starting with a capital letter and 
  containing lower case letters, digits and underline symbols '_'. 
  \para Examples: \ft F \end, \ft Max \end, \ft Power_of_some_prime \end, 
  \ft A1b2c3 \end. 

rem 
  \para \bf  Special notation for functions.  \end 
  \items 
   \item \para Addition \ft x+y \end. 
   \item \para Multiplication \ft x*y \end. 
   \item \para Modified subtraction \ft x-y \end. 
   \item \para Integer division \ft x/y \end. 
   \item \para Remainder function \ft x mod y \end. 
   \item \para Pairing function. \ft x,y \end. 
   \item \para Pair size function \ft |x| \end. 
   \item \para List concatenation \ft x++y \end. 
  \end

rem 
  \para \bf  Special notation for predicates.  \end 
  \items 
   \item \para Less-than comparision predicate \ft x <= y \end. 
   \item \para Strict less-than comparision predicate \ft x < y \end. 
   \item \para Greater-than comparision predicate \ft x >= y \end. 
   \item \para Strict greater-than comparision predicate \ft x > y \end. 
   \item \para List membership predicate \ft x in y \end, its negation 
         \ft x !in y \end. 
  \end

rem 
  \para \bf  ASCII characters and strings.  \end Every character in the extended 
  ASCII set has assigned a value \ft n < 256 \end. For instance, the denotation 
  of the character \ft "a" \end is the number \ft 97 \end, i.e. we have 
  \eq* 
    "a" = 97
  \end
  \para Use the format \ft Ch \end to display numbers as characters, e.g. the 
  result of the simple query 
  \verbatim 
      97 = c:Ch
  \end
  \para is shown as the character \ft "a" \end. Note that the predicate 
  \ft Ch \end is defined in the module \it  Standard  \end. Note also that 
  characters are enclosed in double quotes. 
  \para A finite sequence of extended ASCII characters is called a string. For 
  instance, the string \ft 'abcd' \end denotes the same number as does the 
  sequence \ft "a","b","c","d",0 \end, i.e. we have 
  \eq* 
    'abcd' = "a","b","c","d",0
  \end
  \para Use the format \ft Str \end to display numbers as strings, e.g. the 
  result of the simple query 
  \verbatim 
      97,98,99,100,0 = s:Str
  \end
  \para is shown as the string constant \ft 'abcd' \end. Note that the predicate 
  \ft Str \end is defined in the module \it  Standard  \end. Note also that 
  string constants are enclosed in single quotes. 

rem 
  \para \bf  Formulas.  \end 
  \items 
   \item \para Atomic formulas: \ft x = y \end, \ft R(x) \end. 
   \item \para Propositional connectives: \ft \t \end, \ft \f \end, \ft ~R \end, 
         \ft R & Q \end, \ft R \/ Q \end, \ft R -> Q \end, \ft R <-> Q \end. 
   \item \para Quantifiers: \ft \e yR \end, \ft \a yR \end. 
  \end
  \para Special notation: 
  \items 
   \item \para Inequalities: \ft x != y \end. 
   \item \para Bounded quantifiers: \ft \eb y y <= x: R \end, 
         \ft \ab y y <= x: R \end, \ft \eb y y < x: R \end, 
         \ft \ab y y < x: R \end. 
  \end

rem 
  \para \bf  Section. Explicit Definitions of Predicates.  \end 

rem 
  \para \bf  Bounded formulas.  \end 
  \items 
   \item \para Atomic formulas: \ft x = y \end, \ft R(x) \end. 
   \item \para Propositional connectives: \ft \t \end, \ft \f \end, \ft ~R \end, 
         \ft R & Q \end, \ft R \/ Q \end, \ft R -> Q \end, \ft R <-> Q \end. 
   \item \para Bounded quantification: \ft \eb y y <= x: R \end, 
         \ft \ab y y <= x: R \end, \ft \eb y y < x: R \end, 
         \ft \ab y y < x: R \end. 
  \end
  \para Special notation: \ft x != y \end, \ft x <= y \end, \ft x < y \end, 
  \ft x > y \end, \ft x >= y \end. 

rem 
  \para \bf  Explicit definitions of predicates with bounded formulas.  \end 
  \header* pred/2 Q  \end Example(s): 
  \def 
    pred R 
    R(x) <-> \eb y y <= x: Q(x,y)
  \end
  \def 
    pred R 
    R(x) <-> \eb y y < x: Q(x,y)
  \end
  \def 
    pred R 
    R(x) <-> 
      \ab y y <= x: Q(x,y)
  \end
  \def 
    pred R 
    R(x) <-> 
      \ab y y < x: Q(x,y)
  \end

rem 
  \para \bf  Section. Minimalization.  \end 

rem 
  \para \bf  Definitions of functions with bounded minimalization.  \end 
  \header* pred/2 R  \end Example(s): 
  \def 
    fun F 'Tex_f1_f'
    F(x) = \m y <= x [ R(x,y) ]
  \end
  \def 
    fun F 'Tex_f1_f'
    F(x) = \m y < x [ R(x,y) ]
  \end

rem 
  \para \bf  Definitions of functions with regular minimalization.  \end 
  \header* pred/2 R  \end Example(s): 
  \def 
    fun F 'Tex_f1_f'
    F(x) = \m y [ R(x,y) ]
  \end
  \para provided the following condition of regularity is satisfied: 
  \eq* 
    \a x\e yR(x,y)
  \end

rem 
  \para \bf  Section. Clausal Definitions of Functions.  \end 

rem 
  \para \bf  Assignments.  \end Example(s): \header* fun G 'Tex_f1_g' \end 
  \header* fun/2 H1 'Tex_f2_h' \end 
  \def 
    fun F 'Tex_f1_f'
    F(x) = H1(y,y) <- G(x) = y
  \end

rem 
  \para \bf  Negation discrimination.  \end Example(s): 
  \def 
    fun F 'Tex_f1_f'
    F(x) = Foo <- R(x)
    F(x) = Foo <- ~R(x)
  \end
  \def 
    fun/2 F 'Tex_f2_f'
    F(x,y) = Foo <- x = y
    F(x,y) = Foo <- x != y
  \end

rem 
  \para \bf  Dichotomy discrimination.  \end Example(s): 
  \def 
    fun/2 F 'Tex_f2_f'
    F(x,y) = Foo <- x <= y
    F(x,y) = Foo <- x > y
  \end

rem 
  \para \bf  Trichotomy discrimination.  \end Example(s): 
  \def 
    fun/2 F 'Tex_f2_f'
    F(x,y) = Foo <- x < y
    F(x,y) = Foo <- x = y
    F(x,y) = Foo <- x > y
  \end

rem 
  \para \bf  Discrimination on constant patterns.  \end Example(s): 
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(1) = Foo
    F(2) = Foo
    F(x) = Foo <- x != 0 & x != 1 & x != 2
  \end

rem 
  \para \bf  Discrimination on monadic patterns.  \end Example(s): 
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(x+1) = Foo
  \end
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(1) = Foo
    F(x+2) = Foo
  \end

rem 
  \para \bf  Discrimination on \ft p \end-adic patterns I.  \end Example(s) ( 
  \ft p = 2 \end): 
  \def 
    fun F 'Tex_f1_f'
    F(2*y+0) = Foo
    F(2*y+1) = Foo
  \end
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(2*y+1) = Foo
    F(2*y+2) = Foo
  \end
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(1) = Foo
    F(2*y+2) = Foo
    F(2*y+3) = Foo
  \end

rem 
  \para \bf  Discrimination on \ft p \end-adic patterns II.  \end Example(s) ( 
  \ft p = 2 \end): 
  \def 
    fun F 'Tex_f1_f'
    F(2*y+z) = Foo <- 0 <= z & z <= 1
  \end
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(2*y+z) = Foo <- 1 <= z & z <= 2
  \end
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(1) = Foo
    F(2*y+z) = Foo <- 2 <= z & z <= 3
  \end

rem 
  \para \bf  Discrimination on binary constructor patterns.  \end Example(s): 
  \def 
    fun F 'Tex_f1_f'
    F S0(0) = Foo
    F S0(x) = Foo <- x != 0
    F S1(x) = Foo
  \end
  \def 
    fun F 'Tex_f1_f'
    F S0(x) = Foo <- x = 0
    F S0(x) = Foo <- x != 0
    F S1(x) = Foo
  \end
  \def 
    fun F 'Tex_f1_f'
    F S0(x) = Foo <- x = 0
    F S0(x) = Foo <- x > 0
    F S1(x) = Foo
  \end
  \para Example(s) of syntactically incorrect discrimination: 
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F S0(x) = Foo <- x != 0
    F S1(x) = Foo
  \end
  \def 
    fun F 'Tex_f1_f'
    F S0(0) = Foo
    F S0(x) = Foo <- x > 0
    F S1(x) = Foo
  \end

rem 
  \para \bf  Discrimination on dyadic constructor patterns.  \end Example(s): 
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F S1(x) = Foo
    F S2(x) = Foo
  \end

rem 
  \para \bf  Discrimination on pair patterns.  \end Example(s): 
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(v,w) = Foo
  \end
  \def 
    fun F 'Tex_f1_f'
    F(0) = Foo
    F(u,0) = Foo
    F(u,v,w) = Foo
  \end

rem 
  \para \bf  Section. Clausal Definitions of Predicates.  \end Will be supplied 
  later. 

rem 
  \para \bf  Section. Evaluation.  \end 

rem 
  \para \bf  Queries.  \end Will be supplied later. 

rem 
  \para \bf  Formats.  \end Will be supplied later. 

