Anubis / Anubis

   /**************************************************************************************
   
   
                     _____              ___.   .__         ________  
                    /  _  \   ____  __ _\_ |__ |__| ______ \_____  \ 
                   /  /_\  \ /    \|  |  \ __ \|  |/  ___/  /  ____/ 
                  /    |    \   |  \  |  / \_\ \  |\___ \  /       \ 
                  \____|__  /___|  /____/|___  /__/____  > \_______ \
                          \/ The \/  Anubis  \/    2   \/  Project \/
   
   
   Name of this file:           strong_0 (text file)
   
   Purpose of this file:        Description of ``strong'' types and terms. 
   
   

   Authors (Name [initials]):   Alain Proute'   [AP]
   
   Updates ([initials] (date) comment): 
      [AP] (2007 jun 08) Creation of this file.
   
   
   **************************************************************************************/
   

   ``Strong'' types and terms are the result of interpreting ``weak'' expressions.

   
   
   *** Strong contexts and De Bruijn symbols. 
   
   A strong  context is just a  list of strong types.   In strong items  (types and terms)
   there are  no local  symbols. Instead, there  are ``De  Bruijn'' symbols refering  to a
   depth into the context. Here is how it works. Normally, a context is a list of pairs:
   
                                   [(x_0,T_0),...,(x_k,T_k)]
   
   and the type of  the symbol 'x' is 'T_i' if 'x_i' is the  leftmost occurrence of 'x' in
   the heads of the above list.
   
   The corresponding strong context is just the list:
   
                                          [T_0,...,T_k]
   
   and a symbol, instead of having a name, has just a ``depth''. Such symbols (also called
   ``De Bruijn'' symbols)  will be denoted 's(i)', where 'i' is  the depth indication. So,
   relative to the above strong context, 's(i)'  has type 'T_i' (for all 'i', such that '0
   =< i =< k'). 
   
   From  the stack machine  viewpoint, a  strong context  is just  the description  of the
   stack.  It  indicates  what types  of  data  are  stacked.  Hence,  's(i)' is  just  an
   instruction saying: 'get the datum at depth i in the stack'.
   
   Notice that this does  not imply that all stack slots have the  same size. If each type
   has a well  defined size (number of bits  or bytes needed for any datum  of this type),
   the depths may be computed from these sizes.
   
   
   
   *** Shifting. 
   
   If a strong term 't' is meaningful in a strong context 'G', it is no more meaningful in
   '[U  .  G]',  but  its  ``shifting'' is  (and  represents the  same  thing  in the  new
   context). The result of shifting 't' 'n' times is denoted 't[n]'.
   
   Shifting is very easy to understand from a stack machine view point. Indeed, consider a
   strong term 't' meaningful in some strong context 'G' as a program executable using the
   stack  'G'. If  'n' items  are pushed  on top  of the  stack, the  program 't'  must be
   modified so as to be still executable  with this new stack.  Clearly, the only thing to
   do is  to add  'n' to the  depths of all  free occurrences  of De Bruijn  symbols. This
   operation is called ``shifting by n''.
   
   We will  also have to shift  strong types, since they  may also depend  on symbols, and
   since terms refer  to types. Conversely, shifting of strong  types requires shifting of
   strong terms,  because of witness types.  Hence, the two shifting  algorithms are cross
   recursive.
   
   
   
   *** Replacement. 
   
   We will also have to replace a De Bruijn symbol by a strong term within either a strong
   term or a strong type. The result of replacing the symbol 's(i)' by the term 'a' in 't'
   is denoted: t[a/i]. How it works is defined in details below in this file. 
   
   
   
   
   *** Rules for constructing correct strong contexts, types and terms.
   
   Strong items (contexts, types and terms) are defined using three sorts of ``jugments'',
   which are the following:
   
       /G    meaning that G is a strong context
      T/G    meaning that T is a strong type in (relative to) the (strong) context G
    t:T/G    meaning that t is a strong term of (strong) type T in the (strong) context G
   
   A ``rule'' for defining a strong item is presented as follows:
   
           J_1 ... J_k
           -----------
           J
   
   where J_1,...,J_k are the ``premises'' or ``conditions'' and J is the ``conclusion'' of
   the rule.  The meaning of  the rule is that  J is true  as soon as J_1,...,J_k  are all
   true.
   
   However, the meaning of  these judgements also depend on:
   
     - The global context.
     - A list of parameters.
     - An environment.
   
   We will not represent them explicitely in our rules. 
   
   Each definition in the global context is supposed to be correct.  Hence, each one has a
   meaning, and this meaning  is a strong item (strong type for  a type definition, strong
   term  for a  datum  definition). 

   We may also have  a list of parameters. Each one is  supposed to represent an arbitrary
   correct type. This is the case when we are currently checking a schema. 
   
   We may also have unknowns. Recall that an environment is a list of pairs:
   
                                   [(X_1,T_1),...,(X_k,T_k)]
   
   where each  'X_i' is  an unknown, and  each 'T_i' a  strong type  (there is also  a non
   circularity  condition).   In the  presence  of  this  environment, the  unknown  'X_i'
   represents  the type  'T_i'. Notice  that 'T_i'  may still  contain other  unknowns. Of
   course, any  strong type  or strong term  containing an  unknown is ambiguous  (this is
   called ``parametric ambiguity'').


   
   
      *** Rules for contexts.
   
   - The empty context. [] is a strong context.
   
   ---
   /[]             
   
   
   - Enlargement of contexts. If T is a type relative  to the context G, then [T . G] is a
   strong context.
   
   T/G
   --------
   /[T . G]
    
   
   
   
      *** Rules for types. 
   
   - Strong parameter. It represents a valid arbitrary  type if and only if it is a member
   of the given list of parameters.
   
   
   - Strong unknown. Each unknown represents a type to be determined. Of course, if it has
   a value relative to the current environment, it represents this value. 
   
   
   - Strong defined types.  They  are made of a type id, and a  list of strong types, each
   one corresponding to a parameter of the type having this id.
   
   
   - Strong product types:
   
   T_1/G, ..., T_k/G
   ------------------------
   _Prod(T_1,...,T_k)/G
   
   
   - Strong functional types: Notice that 'U' is a type relative to '[T . G]', not to 'G'.
   This means that 'U' may depend on 'T'. Hence, strong functional types are dependant.
   
   T/G, U/[T . G]
   ------------------       '_Functional(T,U)' is also denoted 'T -> U'
   _Functional(T,U)/G
   
   
   - Strong Omega: '_Omega' is a type in all circumstances. 
   
   /G
   ---------
   _Omega/G
   
   
   
   - Strong witness types: To each strong statement is associated a strong witness type.
   
   E:_Omega/G
   ---------------------
   _Witness(E)/G
   
   
   
   - Strong (universally)  quantified types (Girard's  system F types):  If T is  a strong
   type, and  $X a  parameter, then  '_Quantified($X T)' is  a strong  type (with  no free
   occurrence of the parameter $X).
   
   T/G
   -------------------
   _Quantified($X T)/G
   

public type StrongTerm:...
   
public type StrongType:   
  
   _Parameter        (String name),
   
   _Defined          (Int32            type_id,   
                      List(StrongType) operands), 
   
   _Product          (List(StrongType)), 
   
   _Functional       (StrongType   source, 
                      StrongType   target), 
   
   _Omega, 
   
   _Witness          (StrongTerm statement), 
   
   _Quantified       (String parameter,
                      StrongType). 
   
   
   
   
      *** Rules for terms. 
   
   - De Bruijn symbols: 's(i)' represents the datum at depth 'i' in the context.  The head
   of the context (top of stack) has depth '0'.
   
   
   --------------
   s(0):T/[T . G]
   
   
   s(i):T/G, U/G
   ----------------
   s(i+1):T/[U . G]
   
      
   - Strong   tuples:  A   strong   tuple  has   the   form  'tuple(t_1,...,t_k)',   where
   't_1',...,'t_k' are strong  terms. If the type of 't_i' relative  to the strong context
   'G'   is  'T_i',   then  the   type  of   'tuple(t_1,...,t_k)'  relative   to   'G'  is
   '_Prod(T_1,...,T_k)'.
   

   - t_1:T_1/G,...,t_k:T_k/G
   ---------------------------------------
   tuple(t_1,...,t_k):_Prod(T_1,...,T_k)/G
   
   
   - Strong projections: It 't' is a  strong term of type '_Prod(T_1,...,T_k)', and if 'i'
   is such that '1 =< i =< k', then 'proj(i,t)' is a strong term of type 'T_i'.
   
   t:_Prod(T_1,...,T_k)/G
   ----------------------         for any i such that 1 =< i =< k
   proj(i,t):T_i/G
   
   
   - Strong  inclusions:  Inclusions  are  the  constructors for  sum  types,  i.e.   they
   correspond to  alternatives in  weak types.  Each  alternative has  a type (which  is a
   product type when the re are several components).
   
   If 't' is a term  of type 'T_i', and if 'T_i' is the type  of alternative number 'i' of
   some type 'U', i.e. if U = T_1 + ... + T_k, then 'incl(U,i,t)' is a strong term of type
   'U'.
   
   
   - Strong conditionals:  Conditionals are the  destructors for sum  types.  If 'T'  is a
   strong defined type whose types of alternatives are 'U_1',...,'U_k', if 't' is a strong
   term of type 'T',  if 'V' is a strong type, and if  'c_1',...,'c_k' are strong terms of
   respective types  'U_1 -> V',...,'U_k ->  V', then 'cond(T,t,c_1,...,c_k)'  is a strong
   term of type 'V'.

   t:T/G, c_1:U_1 -> V,...,c_k:U_k -> V
   ------------------------------------
   cond(T,t,c_1,...,c_k):V/G
   
   
   
   - Strong functions: If 'T' is a strong type relative to strong context 'G', if 'E' is a
   strong term of type  'U' relative to '[T . G]', then 'lambda(T,E)'  is a strong term of
   strong type 'T -> U' relative to 'G'.
   
   E:U/[T . G]
   ----------------------
   lambda(T,E):(T -> U)/G
   
   
   
   - Strong applicative  terms: If 'f'  is a strong  term of type 'T  -> U' in  the strong
   context 'G', and if 'a' is a strong  term of type 'T' in the context 'G', 'app(f,a)' is
   a strong  term of type 'U[a/0]'  in the context 'G'.
   
   f:(T -> U)/G, a:T/G
   -------------------
   app(f,a):U[a/0]/G
   
  
   
   - Strong  universally quantified  statements: If  'T' is  a strong  type in  the strong
   context 'G', if  'E' is a strong term of  type '_Omega' in the context  '[T . G]', then
   'forall(T,E)' is a strong term of type '_Omega' in the context 'G'.
   
   E:_Omega/[T . G]
   --------------------
   forall(T,E):_Omega/G
   
   
   In order to declare the three next sorts of strong terms, we need the 'macros' 'exists'
   and 'exists_unique'. They have the same  syntax as 'forall'. They will be defined later
   below.
      
   - strong    description    terms:   If    'p'    is    a    strong   term    of    type
   '_Witness(exists_unique(T,E))', then 'description(p)' is strong term of type 'T'.
   
   p:_Witness(exists_unique(T,E))/G
   --------------------------------
   description(p):T/G
   
   
   - Strong    property    terms:    If    'p'     is    a    strong    term    of    type
   '_Witness(exists_unique(T,E))',   then   'property(p)'   is   strong   term   of   type
   '_Witness(E[description(p)/0])'.
   
   p:_Witness(exists_unique(T,E))/G
   -------------------------------------------
   property(p):_Witness(E[description(p)/0])/G
   
   
   
   - Strong choice terms: If 'p'  is a term of type '_Witness(forall(T,exists(U,E)))' then
   'choice(p)' is a strong term of type: 
   
                _Witness(exists(_Functional(T,U),forall(T,E[app(s(1),s(0))/0]))) 
   
   p:_Witness(forall(T,exists(U,E)))/G
   ----------------------------------------------------------------------------
   choice(p):_Witness(exists(_Functional(T,U),forall(T,E[app(s(1),s(0))/0])))/G
   
   
   
   - Strong parametric terms:
   
   t:T/G
   -------------------------------------          $X any parameter
   parametric($X t):s_Quantified($X T)/G
   
   
   - Strong parametric applicative terms: 
   
   t:_Quantified($X T)/G, U/G
   -----------------------------
   parametric_app(t,U):T[U/$X]/G
   
   
public type StrongTerm:
   global          (Int32 id), 
   symbol          (Int32 depth),             // Nicolaas Govert de Bruijn symbols
   tuple           (List(StrongTerm)), 
   proj            (Int32,   StrongTerm), 
   incl            (StrongType,  Int32,  StrongTerm), 
   cond            (StrongType,  StrongTerm test,  List(StrongTerm) cases), 
   lambda          (StrongType,  StrongTerm), 
   app             (StrongTerm f,  StrongTerm a), 
   forall          (StrongType,  StrongTerm), 
   description     (StrongTerm), 
   property        (StrongTerm), 
   choice          (StrongTerm), 
   parametric      (String parameter,  StrongTerm), 
   parametric_app  (StrongTerm,  StrongType). 
   

   

   
   *** The definition of shifting and replacement.
   
   Since we now know precisely what strong types and terms are, we can define shifting and
   replacement.
   
   _Defined(N,T_1,...,T_k)[n]           is _Defined(N,T_1[n],...,T_k[n])
   _Product(T_1,...,T_k)[n]             is _Product(T_1[n],...,T_k[n])
   _Functional(T,U)[n]                  is _Functional(T[n],U[n])
   _Omega[n]                            is _Omega
   _Witness(E)[n]                       is _Witness(E[n])
   _Quantified($X,T)[n]                 is _Quantified($X,T[n])
   
   
public define StrongType
   shift
     (
       StrongType     t, 
       Int32          n
     ). 
   
   
   Shifting of strong terms sometimes (lambda and forall) requires replacement. 
   
   symbol(i)[n]                         is symbol(i+n)
   tuple(t_1,...,t_k)[n]                is tuple(t_1[n],...,t_k[n])
   proj(i,t)[n]                         is proj(i,t[n])
   incl(T,i,t)[n]                       is incl(T[n],i,t[n])
   cond(T,t,c_1,...,c_k)[n]             is cond(T[n],t[n],c_1[n],...,c_k[n])
   lambda(T,t)[n]                       is lambda(T[n],t[n][symbol(0)/n])
   app(f,a)[n]                          is app(f[n],a[n])
   forall(T,t)[n]                       is forall(T[n],t[n][symbol(0)/n])
   description(t)[n]                    is description(t[n])
   property(t)[n]                       is property(t[n])
   choice(t)[n]                         is choice(t[n])
   parametric(p,t)[n]                   is parametric(p,t[n])
   parametric_app(t,T)[n]               is parametric_app(t[n],T[n])
   
   
public define StrongTerm
   shift
     (
       StrongTerm     t, 
       Int32          n
     ). 


   
   _Defined(N,T_1,...,T_k)[a/i]        is  _Defined(N,T_1[a/i],...,T_k[a/i])
   _Product(T_1,...,T_k)[a/i]          is  _Product(T_1[a/i],...,T_k[a/i])
   _Functional(T,U)[a/i]               is  _Functional(T[a/i],U[a/i+1])
   _Omega[a/i]                         is  _Omega
   _Witness(E)[a/i]                    is  _Witness(E[a/i])
   _Quantified($X T)[a/i]              is  _Quantified($X T[a/i])
   
   
public define StrongType        // returns t[a/i]
   replace
     (
       StrongType    t, 
       StrongTerm    a, 
       Int32         i
     ).
   
      
   symbol(i)[a/i]                     is  a
   symbol(i)[a/j]                     is  symbol(i)         (if i != j)
   tuple(t_1,...,t_k)[a/i]            is  tuple(t_1[a/i],...,t_k[a/i])
   proj(n,t)[a/i]                     is  proj(n,t[a/i])
   incl(U,n,t)[a/i]                   is  incl(U[a/i],n,t[a/i])
   cond(T,t,c_1,...,c_k)[a/i]         is  cond(T[a/i],t[a/i],c_1[a/i],...,c_k[a/i])
   lambda(T,E)[a/i]                   is  lambda(T[a/i],E[a/i+1])
   app(f,b)[a/i]                      is  app(f[a/i],b[a/i])
   forall(T,E)[a/i]                   is  forall(T[a/i],E[a/i+1])
   description(p)[a/i]                is  description(p[a/i])
   property(p)[a/i]                   is  property(p[a/i])
   choice(p)[a/i]                     is  choice(p[a/i])
   parametric($X,t)[a/i]              is  parametric($X,t[a/i])
   parametric_app(t,T)[a/i]           is  parametric_app(t[a/i],T[a/i])
   
   
public define StrongTerm        // returns t[a/i]
   replace
     (
       StrongTerm    t, 
       StrongTerm    a, 
       Int32         i
     ).
   
      
   
   
   
   *** The meaning of witness types. 
   
   As you may see, there is no  constructor for witness types. They are not needed because
   the witness type  '_Witness(forall(T,E))' is equal (say ``by  definition'') to the type
   'T -> _Witness(E)'. This is actually part of the BHK interpretation.
   
   Also remark that 'forall' is the only constructor of type '_Omega'. Since 'forall(T,E)'
   requires an operand 'E'  of type '_Omega', it seems that it  is impossible to construct
   any term  of type '_Omega'.  Actually, this is  not true, and  we may first  define the
   statement 'false' as follows:
   
                                 false := forall(_Omega,s(0))
   
   Notice that  's(0)' is indeed  of type '_Omega',  since according to the  rule defining
   'forall', 's(0)' is to be interpreted relative to the context '[_Omega . G]'. 
   
   The above statement means 'false', because assuming a witness for 'false', we can prove
   any  statement. Indeed, assume  that 'p:_Witness(false)/G',  and 'E:_Omega/G',  then we
   have successively:
   
      p:_Witness(forall(_Omega,s(0)))
      p:_Omega -> _Witness(s(0))
      app(p,E):_Witness(s(0)[E/0])
      app(p,E):_Witness(E)
   
   
   Next, we may define the (non dependant) implication, as follows:
   
                            E:_Omega/G, F:_Omega/G
                            -------------------------------------------------
                            implies(E,F) := forall(_Witness(E),F[1]):_Omega/G
   
   Notice that 'F' must be shifted, in order  to take into account the fact that a witness
   of  'E' has  been pushed  on top  of the  stack.  This  is again  conformal to  the BHK
   interpretation (precisely, the fact that a proof  of 'E => F' is an algorithm producing
   a proof of 'F' from a proof of 'E').
   
   
   This enables to define the statement 'true' as 'false => false':
   
                                true := implies(false,false):_Omega/G
   
   It is  interesting to check that we  are able to prove  'true', i.e. to find  a term of
   type '_Witness(true)'. Here it is:
   
                                    lambda(_Witness(false),s(0))
   
   as you may easily verify. 
   
   
   The next logical connector to be defined is the existential quantifier ('exists'). This
   is done as follows. First of all in the user's Anubis language:
   
                             !x:T E := ?q:Omega ((?x:T (E => q)) => q)
   
   That this is the right definition of 'exists' is well known, and is just a constructive
   version of the classical rule: !x:T E := ~(?x:T ~E), where ~ is the negation. 
   
   As a strong term, this gives the following:
   
    exists(T,E)  := 
       forall(_Omega,(implies(forall(T,implies(replace(shift(E,2),s(0),2),s(2))),s(1))))
   
    i.e. in less formal language: 
   
                     !T E   :=   ?Omega ((?T (E[2][s(0)/2] => s(2))) => s(1))
   
   
   Next, we define the (non dependant) conjunction of 'E' and 'F':
   
                             and(E,F)  :=   exists(_Witness(E),F[1])
   
   Again, we can check that this is conformal to the BHK interpretation, which says that a
   proof of 'E & F' is a pair made of a proof of 'E' and a proof of 'F'. We do it first in
   a less formal  language than the language  of strong terms. Assume that  'p' proves 'E'
   and that 'q' proves 'F'. Then, it is easy to verify that the following is a proof of 'E
   & F':
   
                     (y:Omega) |-> (r:W(?x:W(E) (F => y))) |-> r(p)(q)
   
   i.e. of  E & F := ?y:Omega  ?r:W(?x:W(E) F => y)  y.  Conversely, assume that  'p' is a
   proof of 'E & F'. Then, 'p(E)' is a proof of '?r:W(?x:W(E) (F => E)) E'. Now, since
   
                                  s := (x:W(E)) |-> (y:W(F)) |-> x
   
   is a proof of  '?x:W(E) (F => E)', we see that 'p(E)(s)' is  a proof of 'E'. Similarly,
   'p(F)' is a proof of '?r:W(?x:W(E) (F => F)) F'. Since, 
   
                                  t := (x:W(E)) |-> (y:W(F)) |-> y
   
   is a proof of '?x:W(E) (F => F)', we see that 'p(F)(t)' is a proof of 'F'. 
   
   All the above may be rewritten in the language of strong terms (this is an exercice).
   
   
   Next, following Leibnitz, we define the equality like this:
   
      equals(a,b)  := 
             forall(_Functional(T,_Omega),implies(app(s(0),a),app(s(0),b)))

   This definition just says  that 'a' is equal to 'b' if and only  if any property of 'a'
   is also a property of 'b'. Despite its apparently asymmetric aspect, this definition is
   actually symmetric.
   
   
   Finally, we have to define 'exists_unique'. This is done as follows:
   
    exists_unique(T,E)  := 
                  exists(T,and(E,forall(T,implies(E,equals(s(0),s(1))))))
   
   

   
   
   *** Dependant conjunction and implication. 
   
   It is possible to define a dependant conjunction and a dependant implication. This will
   give a meaning to 'E & F' and 'E => F' in the case where 'E:Omega/G' and 'F:Omega/[W(E)
   .  G]', i.e.  when  'F' depends  on  a witness  of  'E'. This  situation  is common  in
   mathematics and in the natural language. 

   We have already seen the rule for non dependant implication:
   
                    E:_Omega/G, F:_Omega/G
                    -------------------------------------------------
                    implies(E,F) := forall(_Witness(E),F[1]):_Omega/G
   
   The rule for dependant implication is the following:
   
                    E:_Omega/G, F:_Omega/[_Witness(E) . G]
                    --------------------------------------------------
                    dep_implies(E,F) := forall(_Witness(E),F):_Omega/G
   
   The difference is just that 'F' being meaningful in the context '[_Witness(E) . G]', it
   should not be shifted.
   
   The same thing works for the conjunction. Just use 'exists' instead of 'forall':
   
                    E:_Omega/G, F:_Omega/[_Witness(E) . G]
                    ----------------------------------------------
                    dep_and(E,F) := exists(_Witness(E),F):_Omega/G
   
   
   
   
   *** The disjunction and the negation. 
   
   The disjunction (logical 'OR')  is never dependant. It is defined as  follows in a less
   formal language:
   
                     E | F := ?q:Omega ((E => q) => ((F => q) => q))
   
   Again, this is the constructive variant of the well known De Morgan's law: 
   
                                     'E | F = ~(~E & ~F)'.
   
   
                    E:_Omega/G, F:_Omega/G
                    -------------------------------------------------------------
                    or(E,F) := forall(_Omega,
                                 implies(implies(E[1],s(0)),
                                         implies(implies(F,s(0))),s(0))):_Omega/G
   
   
   The negation '~E'of 'E' is just 'E => false':
   
                    E:_Omega/G
                    ----------------------------
                    neg(E) := implies(E,false)/G
   
   
   
   
   *** Handling ambiguities and errors. 
   
   Because of the possibility of overloading the symbols, and the presence of type
   parameters, expressions may be ambiguous. There are two kinds of ambiguity:
   
     - simple ambiguity:      a symbol may have several definitions, 
     - parametric ambiguity:  an expression may depend on an unknown type. 
   
   In order to handle these ambiguities, we must be able to manipulate:
   
     - meta-disjunctions of strong items, 
     - unknowns
   
   For example, if the symbol x has three definitions D_1, D_2, and D_3, its
   interpretation will be the meta-disjunction:
   
      D_1 | D_2 | D_3
   
   Later, the unification may lead to eliminate some possibilities in this
   meta-disjunction.
   
   Type unknowns are created each time we use a schema. If for example the symbol x has a
   definition depending on a parameter $T, we create a new unknown, say $567, and use as a
   possible interpretation of x the result of replacing the parameter $T by the unknown
   $567 in this definition.

   We also introduce a special element ``none'' representing the impossibility to
   interpret a weak expression. Notice the analogy between:
   
         this                  and this
         ----------------------------------
         none                  false
         meta-disjunction      or
         unknowns              there exists
   
   Also remark that 'false', 'or' and 'exists' are the three usual ``additive'' connectors
   in logic. Of course, all this is not a hazard.
   
   So, we have to consider a notion somewhat weaker than a strong type, and similarly a
   notion somewhat weaker than a strong term. These notions have the same definitions as
   strong types and strong terms, except than they include the concepts of 'none', and
   'unknown' for types, and of 'none' and 'meta-disjunction' for terms.  Since these
   notions are precursors of strong items, we will call them ``pre-strong'' items.

   
public type PreStrongTerm:...
   
public type PreStrongType:
   _None,
   _Unknown          (Int32),
   _Parameter        (String name),
   _Defined          (Int32            type_id,   
                      List(PreStrongType) operands), 
   _Product          (List(PreStrongType)), 
   _Functional       (PreStrongType   source, 
                      PreStrongType   target), 
   _Omega, 
   _Witness          (PreStrongTerm statement),    
   _Quantified       (String parameter,
                      PreStrongType). 
   
   
   
public type PreStrongTerm:
   none,
   meta_or           (PreStrongTerm,  PreStrongTerm),
   symbol            (Int32 depth),            
   tuple             (List(PreStrongTerm)), 
   proj              (Int32,PreStrongTerm), 
   incl              (PreStrongType,  Int32,  PreStrongTerm), 
   cond              (PreStrongType,  PreStrongTerm test,  List(PreStrongTerm) cases), 
   lambda            (PreStrongType,  PreStrongTerm), 
   app               (PreStrongTerm f,  PreStrongTerm a), 
   forall            (PreStrongType,  PreStrongTerm), 
   description       (PreStrongTerm), 
   property          (PreStrongTerm), 
   choice            (PreStrongTerm), 
   parametric        (String parameter,  PreStrongTerm), 
   parametric_app    (PreStrongTerm,  PreStrongType).