% $Id: ELF.lsl,v 1.5 2000/04/19 06:41:36 connolly Exp $
%

A Framework for Defining Logics cited from PCA


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]) Î 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 á deq(G, S) ñ Kp
    Þ has_kind(A, Kp)[G, S];

% Valid Objects

% B-CONST-OBJ
    valid_context(G, S)
    Ù family([c, A]) Î S
    Þ has_type(\const c, A)[G, S];

% B-VAR-OBJ
    valid_context(G, S)
    Ù [x, A] Î 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 á deq(G, S) ñ 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...

[Index]

[source]

HTML generated using lsl2html.