[SCL] two comments

[Robert E. Kent]

Pat Hayes wrote:

    Guys, I was using the term 'abstract syntax' in a
    precise sense. It is a technical term introduced
    by John McCarthy; its not just a handy English
    phrase. See
    http://www-formal.stanford.edu/jmc/towards/node12.html
    for a succinct introduction.  This approach was
    later formalized and systematized in the
    specification literature as 'term algebras', I
    believe, but we don't really need to get that
    formal.

    The key motivational point is stated economically there:

    " The predicates and functions whose existence
    and relations define the syntax, are precisely
    those needed to translate from the language, or
    to define the semantics. That is why we need not
    care whether sums are represented by a+b, or +
    ab, or (PLUS A B), or even by Gödel numbers
    7a11b."

    which is exactly the utility for us, since we
    want to allow things like CG diagrams to count as
    logical syntax. In Murray's terminology, the AS
    is the highest meta-level anyone needs to go to
    in order to define a syntax and a model theory.
    (Splicing together documents, now, is another
    matter....)


The orientation in McCarthy's web page "Abstract Syntax of Programming
Languages" seems to be towards *abstract data types*, which define
axiomatizations for data types. The classic case is the stack data type,
where one axiomatization goes as follows:

1. Since this is parametric, there is a name for the parameter type 'P'.

2. There is a name for stacks, say 'Stack(P)'.

3. There is a collection of synthetic/constructor operators on stacks:

empty : Stack(P)
push : P × Stack(P) --> Stack(P)

4. There is a collection of analytic/selector operators on stacks:

is-empty : Stack(P) --> Boolean
is-nonempty : Stack(P) --> Boolean
top : Stack(P) --> P
pop : Stack(P) --> Stack(P)

5. These operators satisfy the defining stack abstract data type semantics:

is-empty(empty)
forall (p:P, s:Stack(P)) is-nonempty(push(p,s))
top(push(p,s)) = p
pop(push(p,s)) = s

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

Turning now towards SCL, we seem to need an SCL term abstract data type and
an SCL formula abstract data type, with SCL formulas defined in terms of SCL
terms.

(For simplicity, I will just express the traditional FOL part, I do not
express the SCL term operators or SCL term abstract data type semantics, and
I only express some of the SCL formula abstract data type semantics.)

SCL terms:
...

SCL formulas:

1. There is a parameter lexicon L.

2. There is a name for SCL formulas 'Fla(L)'.

3. There is a collection of synthetic/constructor operators on SCL formulas:

Holds = makeAtom : union_{n \in Natno) Pred(L,n)  × Trm(L,n) --> Fla(L)
Id = makeEqn : Trm(L) × Trm(L) --> Fla(L)
Neg = makeNeg : Fla(L) --> Fla(L)
Conj = makeConj : Fla(L)* --> Fla(L)
Disj = makeDisj : Fla(L)* --> Fla(L)
Cond = makeCond : Fla(L) × Fla(L) --> Fla(L)
BiCond = makeBicond : Fla(L) × Fla(L) --> Fla(L)
ExQuant = makeExQuant : GenVar(L) × Fla(L) --> Fla(L)
UnivQuant = makeUnivQuant : GenVar(L) × Fla(L) --> Fla(L)

4. There is a collection of analytic/selector operators on SCL formulas:

isAtom : Fml(L) --> Boolean
pred : Fla(L) --> Pred(L)
trmSeq : Fla(L) --> Trm(L,n)
isEqn : Fla(L) --> Boolean
firstTerm : Fla(L) --> Trm(L)
secondTerm : Fla(L) --> Trm(L)
isNeg : Fla(L) --> Boolean
negFla : Fla(L) --> Fla(L)
isConj : Fla(L) --> Boolean
conjunct : Fla(L) × Natno --> Fla(L)
isDisj : Fla(L) --> Boolean
disjunct : Fla(L) × Natno --> Fla(L)
isCond : Fla(L) --> Boolean
antecedent : Fla(L) --> Fla(L)
consequent : Fla(L) --> Fla(L)
isBiCond : Fla(L) --> Boolean
firstEquivalent : Fla(L) --> Fla(L)
secondEquivalent : Fla(L) --> Fla(L)
isExQuant : Fla(L) --> Boolean
exBoundVar : Fla(L) --> GenVar(L)
exQuantFla : Fla(L) --> Fla(L)
isUnivQuant : Fla(L) --> Boolean
univBoundVar : Fla(L) --> GenVar(L)
univQuantFla : Fla(L) --> Fla(L)

5. These operators satisfy the defining SCL formula abstract data type
semantics:

(I write only some of the axioms)

forall (p:Pred_n(L), t:Trm(L,n))
    isAtom(Hold(p,t))

forall (p:Pred_n(L), t:Trm(L,n))
    (atomPredicate(Hold(p,t)) = p
    and
    atomTermSequence(Hold(p,t)) = t)

forall (t1:Trm(L), t2:Trm(L))
    (firstTrm(Id(t1,t2)) = t1
    and
    secondTrm(Id(t1,t2)) = t2)

forall (f1:Fla(L), f2:Fla(L))
    (antecedent(Cond(f1,f2)) = f1
    and
    consequent(Cond(f1,f2)) = f2)

etc.

Of course, we can specify fixpoint set equations for both SCL terms and SCL
formulas in order to constructively generate the synthetic operators.

Robert E. Kent
rekent at ontologos.org