% $Id: ELF.lsl,v 1.5 2000/04/19 06:41:36 connolly Exp $
%
%html <p><a href="http://www.dcs.ed.ac.uk/lfcsreps/91/ECS-LFCS-91-162/">A Framework for Defining Logics </a>
%html cited from <a href="http://www.cs.princeton.edu/sip/projects/pca/">PCA</a></p>

ELF: trait
  includes
    Set(Constant, Set[Constant]),
    Set(Variable, Set[Variable]),
    List(ConstantBinding, Signature),
    List(VariableBinding, Context),
    Relation(Kind, Rel[Kind]),
    Relation(Family, Rel[Family]),
    Relation(Object, Rel[Object])
    
  Term union of K: Kind, A: Family, M: Object
  ConstantBinding union of kind: KindBinding, family: FamilyBinding
  KindBinding tuple of a: FamilyConstant, K: Kind
  FamilyBinding tuple of c: ObjectConstant, A: Family
  Constant union of a: FamilyConstant, c: ObjectConstant
  VariableBinding tuple of x: Variable, A: Family

introduces
  Type : -> Kind
  Pi : Variable, Family, Kind -> Kind

  \const __ : FamilyConstant -> Family
  Pi: Variable, Family, Family -> Family
  lambda: Variable, Family, Family -> Family
  __ \juxt __ : Family, Object -> Family % juxtaposition; i.e. A M

  __ => __: Family, Family -> Family

  \const __ : ObjectConstant -> Object
  \var __ : Variable -> Object
  lambda: Variable, Family, Object -> Object
  __ \juxt __ : Object, Object -> Object


  subst: Object, Variable, Object -> Object %@@axioms for subst? p. 6
  subst: Object, Variable, Kind -> Kind
  subst: Object, Variable, Family -> Family

  dom: Signature -> Set[Constant]
  dom: Context -> Set[Variable]

  sig: Signature -> Bool % __ is a valid signature

  __ [__, __]: CSBool, Context, Signature -> Bool
  valid_context: Context, Signature -> Bool
  valid_kind: Kind -> CSBool
  has_kind: Family, Kind -> CSBool
  has_type: Object, Family -> CSBool

  deq: Context, Signature -> Rel[Kind]
  deq: Context, Signature -> Rel[Family]
  deq: Context, Signature -> Rel[Object]

asserts
  Kind generated by Type, Pi
  Family generated by \const, Pi, lambda, \juxt
  Object generated by \const, \var, lambda, \juxt
  CSBool generated by valid_kind, has_kind, has_type

  forall x, y, z: Variable, c, d: ObjectConstant, a, b: FamilyConstant,
	S: Signature, G: Context,
	A, B, Ap: Family, K, Kp: Kind, M, N: Object

  % Valid Signatures

    sig(empty);

    dom(empty:Signature) = {};
    dom(S \postcat kind([a, K])) = insert(a(a), dom(S));
    dom(S \postcat family([c, A])) = insert(c(c), dom(S));

    dom(empty:Context) = {};
    dom(G \postcat [x, A]) = insert(x, dom(G));

    sig(S) /\ valid_kind(K)[empty, S] /\ a(a) \notin dom(S)
      => sig(S || {kind([a, K])});

    sig(S) /\ has_kind(A, Type)[empty, S] /\ c(c) \notin dom(S)
      => sig(S || {family([c, A])});

  % Valid Contexts

    sig(S) => valid_context(empty, S);

    valid_context(G, S)
    /\ has_kind(A, Type)[G, S]
    /\ x \notin dom(G)
    => valid_context(G \postcat [x, A], S);

  % Valid Kinds

    valid_context(G, S)
    => valid_kind(Type)[G, S];

    valid_kind(K)[G \postcat [x, A], S]
    => valid_kind(Pi(x, A, K))[G, S];

  % Valid Families

    % B-CONST-FAM
    valid_context(G, S)
    /\ kind([a, K]) \in S %@@paper says c, but shouldn't it be a???
    => has_kind(\const a, K)[G, S];

    % B-PI-FAM
    has_kind(B, Type)[G \postcat [x, A], S]
    => has_kind(Pi(x, A, B), Type)[G, S];

    % B-ABS-FAM
    has_kind(B, K)[G \postcat [x, A], S]
    => has_kind(lambda(x, A, B), Pi(x, A, K))[G, S];

    % B-APP-FAM
    has_kind(A, Pi(x, B, K))[G, S]
    /\ has_type(M, B)[G, S]
    => has_kind(A \juxt M, subst(M, x, K))[G, S];

    % B-CONV-FAM
    has_kind(A, K)[G, S]
    /\ valid_kind(Kp)[G, S]
    /\ K \langle deq(G, S) \rangle Kp
    => has_kind(A, Kp)[G, S];

  % Valid Objects

    % B-CONST-OBJ
    valid_context(G, S)
    /\ family([c, A]) \in S
    => has_type(\const c, A)[G, S];

    % B-VAR-OBJ
    valid_context(G, S)
    /\ [x, A] \in G
    => has_type(\var x, A)[G, S];

    % B-ABS-OBJ
    has_type(M, B)[G \postcat [x, A], S]
    => has_type(lambda(x, A, M), Pi(x, A, B))[G, S];

    % B-APP-OBJ
    has_type(M, Pi(x, A, B))[G, S]
    /\ has_type(N, A)[G, S]
    => has_type(M \juxt M, subst(N, x, B))[G, S];

    % B-CONV-OBJ
    has_type(M, A)[G, S]
    /\ has_kind(Ap, Type)[G, S]
    /\ A \langle deq(G, S) \rangle Ap
    => has_type(M, Ap)[G, S];


    equivalence(deq(G, S):Rel[Kind]);
    equivalence(deq(G, S):Rel[Family]);
    equivalence(deq(G, S):Rel[Object]);

  % table 3: parallel reduction @@

  implies
  % Theorem 2.3

  forall G, Gp: Context, S: Signature, alpha: CSBool

    % 1. weakening
    alpha[G, S]
    /\ valid_context(G || Gp, S)
    => alpha[G || Gp, S];

    % others...