% $Id: ContextLogic.lsl,v 1.2 2001/05/17 17:28:05 connolly Exp $
%
%html <cite><a href="http://www-formal.stanford.edu/guha/guha-thesis.ps">Contexts: A Formalization and Some Applications</a></cite>;
%html from <a href="http://www-formal.stanford.edu/guha/">Guha's page at stanford</a>
%html <hr />

ContextLogic: trait
  includes
    FormalSystem,
    List(Term),
    List(Object),
    FiniteMap(Symbol, Object),
    Integer

    % p 20 Grammaticality
    Term union of s: Symbol, app: Application

    Application tuple of f: Symbol, args: List[Term]

    Atomic tuple of p: Symbol, args: List[Term]

    CFormula union of a: Atomic,
                     notF: FormulaAux,
                     andFG: FormulaPair,
                     allXF: VarWithFormula,
                     orFG: FormulaPair,
                     eqXY: TermPair,
                     ifFG: FormulaPair,
                     ist: ContextWithFormula

    FormulaAux tuple of f: CFormula
    FormulaPair tuple of f, g: CFormula
    VarWithFormula tuple of v: Symbol, f: CFormula
    TermPair tuple of x, y: Term
    ContextWithFormula tuple of ck: Context, P: CFormula


  introduces

    % 2.1.2 Syntax and Semantics, p. 20
    % (1) contexts
    isContext: Object -> Bool
    obj: Context -> Object % subsort
    G95: ContextStructure, Context -> System

    % (2) Grammaticality
    x: CFormula -> Formula % subsort

    isVar: Symbol -> Bool % hmm... I'd like this to depend on the context...

    % (3) Language
    in: Symbol, Language -> Bool
    arityF: Symbol, Language -> Int
    arityP: Symbol, Language -> Int

    % (4) Interpretation
    indiv: Interpretation, Symbol -> Object
    func: Interpretation, Symbol -> Func
    value: Func, List[Object] -> Object
    pred: Interpretation, Symbol -> Relation
    in: List[Term], Relation -> Bool

    % where did (5) go???

    % (6) Context Structure
    L: ContextStructure, Context -> Language
    CM: ContextStructure, Context, Interpretation -> Bool

    % (7) meaningful: we use wff...
    meaningful: CFormula, Context, ContextStructure -> Bool

    % (8) substitution
    subst: Map[Symbol, Object], Interpretation, Term -> Object
    substN: Map[Symbol, Object], Interpretation, List[Term] -> List[Object]

    % (9) satisfaction
    satisfies: Interpretation, ContextStructure, Map[Symbol, Object],
	       CFormula, Context -> Bool
    satisfiesFOL: Interpretation, ContextStructure, Map[Symbol, Object],
	       CFormula, Context -> Bool
    satisfiesIST: Interpretation, ContextStructure, Map[Symbol, Object],
	       CFormula, Context -> Bool


  asserts
    % (1) Contexts
    forall C: Context

    isContext(obj(C))

    % (3) Language
    forall l: Language, s, p: Symbol,
	   os: List[Object],
	   C: Context, CS: ContextStructure,
	   args: List[Term],
	   F, F1, F2: CFormula

    % arityF <= 0 -> not a function symbol
    % arityP <= 0 -> not a predicate symbol
    % both 0: individual
    % both < 0: variable or not in this language
    isVar(s) => (arityF(s, l) < 0 /\ arityP(s, l) < 0);
    in(s, l) => ((arityF(s, l) = 0) \/ (arityP(s, l) = 0));
    in(s, l) <=> arityF(s, l) >= 0;
    in(s, l) <=> arityP(s, l) >= 0;

    % (7) meaningful, and wff
    x(F1) = x(F2) => F1 = F2;
    
    wff(G95(CS, C), x(F)) <=> meaningful(F, C, CS);

    meaningful(F, C, CS) => arityP(p, L(CS, C)) = len(args);

    %@@similarly for arity of args of function application in terms...

    % (8) substitution
    forall S: Map[Symbol, Object], U: Interpretation, x, x1: Term, xn: List[Term]

    subst(S, U, x) = (if tag(x) = s
		      then if isVar(x.s) then apply(S, x.s)
			   else indiv(U, x.s)
		      else value(func(U, x.app.f), substN(S, U, x.app.args)));
    substN(S, U, empty) = empty;
    substN(S, U, x1 -| xn) = subst(S, U, x1) -| substN(S, U, xn);

    % (9) satisfaction

    forall F: CFormula, S: Map[Symbol, Object],
	   C, Ck: Context, CS: ContextStructure, U, Uj: Interpretation,
	   ck: Term

    satisfies(U, CS, S, F, C) <=>
     (    CM(CS, C, U)
       /\ meaningful(F, C, CS)
       /\ (if tag(F) ~= ist then satisfiesFOL(U, CS, S, F, C)
	                    else satisfiesIST(U, CS, S, F, C) ) );

    tag(F) ~= ist =>
    (satisfiesFOL(U, CS, S, F, C) <=>
      (     if tag(F) = a    then in(F.a.args, pred(U, F.a.p))
       else if tag(F) = notF then not satisfies(U, CS, S, F.notF.f, C)
       else if tag(F) = andFG then (   satisfies(U, CS, S, F.andFG.f, C)
				    /\ satisfies(U, CS, S, F.andFG.g, C))
       else if tag(F) = orFG then (    satisfies(U, CS, S, F.orFG.f, C)
				    \/ satisfies(U, CS, S, F.orFG.g, C))
       else if tag(F) = ifFG then (not satisfies(U, CS, S, F.ifFG.f, C)
				   \/  satisfies(U, CS, S, F.ifFG.g, C))
       else if tag(F) = eqXY then (subst(S, U, F.eqXY.x) =
				   subst(S, U, F.eqXY.y))
       else false
      ));

    %tag(F) = ist /\ obj(Ck) = subst(S, U, F.ist.ck) =>
    %(satisfiesIST(U, CS, S, F, C) <=>
    %  \forall Uj ( @@@hmm... what's the syntax for forall inside a formula
    % in larch?