% $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.