A top-level ontology of structures for KRL models

Dr Ph. MARTIN

This document mixes HTML and FL (a KRL, i.e., a Knowledge Representation Language; it is here used in the preformatted text parts). It is an input+backup+presentation file for the Multi-Source Ontology (MSO). The MSO  i) aligns and extends several ontologies, and  ii) can be extended by Web users via the shared KB server WebKB-2 and its shared KB (knowledge base) editing protocols.
In this document, for supertype links, "/^" is used instead of the more common "<" symbol.
Similarly, for subtype links, "\." is used instead of the more common ">" symbol.
Link is used as a short synonym for "binary relation" or, more precisely, for an abstract element that represents a binary relation.

The ontology in this document is original.
It is part of a set of complementary "ontologies on formal languages":

The goals, underlying ideas, conventions and content of these ontologies are explained and illustrated in this article (some figures of these articles are pointed to at the end of some section titles below since synthetic graphical illustrations may ease the undestanding of the textual representations).
These ontologies use a much more generic approach than the one of my earlier attempts at representing some KRL models and notations:
- the section 4.5.1 of my HDR (meta-model)
- the section 2.1.3. of my HDR (tables 2.1.3.1 to 2.1.3.5).


Table of contents

0.  Language_element     (figure)
    0.1.  Language_element w.r.t. other top-level types
    0.2.  Top-level relation types for Language_element
    0.3.  First subtypes of Abstract_element (AE)
        0.3.1.  First partitions for AEs
        0.3.2.  Phrase
        0.3.3.  Referring_AE_or_NR-phrase
    0.4.  Functions for easing the use of relation types from Section 0.2

1.  NR_phrase (or component of it)     (figure)
    1.1.  Modularizing_NR_phrase
    1.2.  NR_formula

2.  Value (structured or not) or reference (to a phrase or not)
    2.1.  Operator (function type, ...)
    2.2.  Structured Value
    2.3.  Value token


0.  Language_element     (figure)

In the FL representations below, characters in bold or italics are only for easing understanding: HTML markup is ignored by the FL interpreter.
In this KRL ontology, pm is the default author (hence the author of unprefixed elements).
As opposed to the figure, the names of relation types from pm are prefixed by "r_" instead of "has_".


0.1.  Language_element w.r.t. other top-level types

In this section, italic characters are used for types prefixed by "pm#sbvr#", i.e., SBVR types as understood by pm. The meaning of some types of the SBVR ontology would be clearer if, as in KRLO, it used distinctions/types such as Description_content, Description_instrument and Description_container.

Thing = owl#Thing  "anything that exists or that can be thought about is a Thing",
 := [any ?x  r_type: Thing],
 r_description: 0..* Description_content-or-instrument-or-container,
 r_description_instrument: 0..* Language_or_language-element,
 \. partition
    { (Situation  = "Thing that may occur",
                  r_description_instrument: 0..* Phrase,
        \. partition
           { (State   = "Situation that is not a Process")
             (Process = "Situation that is making a change",
               \. dolce#Perdurant
                  (Presenting  r_physical_medium: 1..* Physical_medium) )
           } ) 
      (Entity = "any Thing that can be 'involved' in a situation, i.e.,"+
                " that may 'participate' to it; this cannot be a Situation",
        \. partition
           { (Spatial_object
               \. partition { (Physical_entity  \. Physical_medium) //e.g., Paper, USBS_key
                              Spatial_non-physical_entity   //e.g., Square
                            } )
             (Non-spatial_object  //e.g., Justice, Attribute, ...
               \. partition
                  { (Attribute_or_quality_or_measure 
                      \. Presenting_attribute-or-quality-or_measure )
                    (Non-spatial_object_that_is_not_an_attribute-or-quality-or-measure
                      \. (Description_content-or-medium-or-container
                            r_physical_medium: 1..* Physical_medium,
                            \. (Description_content = pm#sbvr#Meaning,
                                  r_description_instrument: 0..* Description_instrument,
                                  \. pm#sbvr#Proposition  pm#sbvr#Question  )
                               (Description_container  \. (File \. RDF_file))
                               (Description_instrument
                                  r_description_container:  0..* Description_container,
                                  \. Language_or_language-element  //see below
                               ) ) )
                  } )
           } )
    }
    partition
    { (First_order_thing
         \. partition 
            { (Individual_thing = First_order_concept_thing, 
                 r_description_instrument: 0..* Individual ) //see "Individual" below
              (Relation_thing 
                 r_description_instrument: 0..* r_relation ) //see "r_relation" below
            } )
      (Type_as_description_content //such a type is not a type of language element
           //in the above cited figure, this type is named "TypeDc"
        r_description_instrument:   //the following types are types of AEs (hence of language elements)
          (Type = Type_expression  Type_as_description_instrument  Type_as_AE
                //in the above cited figure, this type is named "Type_AE"
             /^ Reference-token_or_structured-value_or_type,   //Section 0.3.3
             \. pm#sbvr#Noun_concept  (pm#sbvr#Verb_concept = pm#sbvr#Fact_type)
                partition
                { Type_that_is_not_a_reference  //just to be complete; probably not needed
                  (Reference_to_type  r_result=: 1 Type_that_is_not_a_reference,
                    \. (IRI_referring_to_type /^ IRI) )
                }
            
                partition  //even though Relation_type /^^ Concept_type
                { (Concept_type = Class, //\. rdfs#Class, //rdfs#Datatype is subtype+instance
                     \. partition     //e.g., in RDF, all datatypes are classes
                        { (Value-token_type //= rdfs#Datatype      cf. Section 2.3
                            \.. Value_token ) //= rdfs#Literal, Typed_value_token or not
                          (Description-or-reference-or-structure_type
                            \.. xs#language
                                Function_call // /^ Structured_referring_AE  //cf. Section 0.3.3
                                (Function_call_type = Function,  \.. Function_call,
                                  \. partition{ Selection_function Generation_function } )
                              //(Type_definition \. Function_type_definition) //Section 0.3.2
                          ) 
                        }
                        Anonymous_concept_type
                        (Constant_type \. partition{Value-token_type  Identifier_type})
                        owl#Nothing 
                  )
                  (Relation_type  \.. r_relation,
                     \. (Binary-relation_type  \.. r_binary_relation,
                          \. (Property_type /* = rdf#Property */)  Binary_predicate
                             Transitive_relation_type
                        )
                        Functional_relational_type )
                } 
               
          ) )
    };

  Language_or_language-element
    \. partition 
       { (Language  r_member: 1..* Language_element,
           \. partition
              { (Language_abstract-model = Language_model,
                   r_member:= only ^(Language_element descr_instr of: 1..* AE),
                   \. KRL_model Abstract_grammar ),
                (Language_concrete-model = Language_notation, 
                   r_member:= only ^(Language_element descr_instr of: 1..* CE),
                   \. KRL_notation  Concrete_grammar ),
              }
              (KRL = Knowledge_representation_language,
                \. %{ KRL_model  KRL_notation },
                r_KRL of: 1..* Language_element )
              (Grammar  r_member: 1..* Grammar_element,
                \. %{ Abstract_grammar  Concrete_grammar },
                r_grammar_head_type: Document ),< !-- //no more Grouped_phrases -->
         )
         (Language_element        //-> grammar token  
           = formal_document-element,  //  (lexical or not) grammar 
           r_representation of: 1..* Thing, //pm#sbvr#Meaning
           \. //the next set is not a "partition" since
              // 1. things like strings and characters can be seen as both AEs and CEs;
              //    in fact, by default in KRLO, the type CE is a subtype of Value_token;
              // 2. some users may need to see each CE as an instance of the AE it represents;
              //    they may add:  r_CE /^ r_instance;  //hence:  rc_type /^ r_subtype;
             %{ (Abstract_element = AE, //already represented:   /^^ AE_type,
                   \. (Link r_descr_instrument of: r_binary_relation),
                   r_CE: 0..* Concrete_element  //for some users:  r_CE /^ r_instance;
                )  
                (Concrete_element = CE //what any (lexical or not) concrete grammar defines
                   r_CE of: 0..* Abstract_element, 
                   \. partition 
                      { (CE_and_AE \. Value_token)   CE_and_not_AE }
                      partition  //details in ../o_KRLnotationTop/d_KRLnotationsTop.html
                      { CE_for_a_token
                        (CE_for_non-token_AE  \. CE_part_of_token)
                      }
                      partition 
                      { Non-structured_CE
                        (Structured_CE
                          \. (pm#sbvr#Expression  \. pm#sbvr#Text) )
                      } )
              }
              partition
              { (Positional_language_element = "Language_element whose parts are only"+
                                               " distingued via their order" )
                (Non-positional_language_element
                  \. Language_element_with_named_arguments  Frame_element)
              }
         )
       };


0.2.  Top-level relation types for Language_element

r_relation ~[Thing, Thing]
 \. (r_relation_from_description-or-thing_that-should_be  //since many KRL models do not
      \. r_relation_from_description                      //  make this distinction
         (r_relation_from_or_to_description-or-thing_that-should_be
           \. (r_relation_from_or_to_AE-or-thing_that-should_be
                \. partition
                   { (r_relation_from_AE-or-thing_that-should_be
                       \. (r_relation_from_and_to_AE-or-thing_that-should_be
                             \. r_relation_for_module_context
                                (r_reification_relation \. r_reification_relation_to_AE)
                                r_relation_from_collection_to_AE-or-thing_that-should_be )
                     )
                     (r_relation_to_AE-or-thing_that-should_be
                       \. r_relation_from_and_to_AE-or-thing_that-should_be
                          r_relation_to_value-or-thing-that-should-be )
                     )
                   }
                   r_relation_from_or_to_type-or-thing_that-should_be //see end of section
              )
         )
    )
    (r_relation_to_description-or-thing_that-should_be
      \. r_relation_to_description
         (r_relation_from_or_to_value-or-thing_that-should_be \. r_value)
    )
    (r_different = "!=")   (r_equal = "=")
    (r_equivalent_thing = "<=>",  \. r_equivalent_phrase  r_equivalent_type)
    (r_annotation 
      \. r_annotation_without_link ~(AE_that_can_be_annotated_without_link,
                                     AE_that_can_be_annotation_value ) )
    r_definition
    (r_direct-or-not_part ~[?e ?part] = r_part,          
      := [or_{ [?e r_direct_part: ?part],  [?e r_direct_member: ?part],
               [?e r_direct-or-not_part: (a Thing  r_direct-or-not_part: ?part)] }],
      /^^ Transitive_relation_type,
      \. partition { r_direct_part  r_direct_member },
         (r_direct-or-not_part_of_same_type ~[?e ?part]
           := [ [?e r_type: ?t, r_part: ?part] =: [?part r_type: ?t] ] )
         (r_sub_KRL_model ~[KRL_abstract_model  KRL_abstract_model] 
            //structural AND semantic part sub-model; not used in 
            // "OWL_model r_part_type: RDFS"  since not every OWL_model semantically includes
            // the semantics of RDFS
    )                     
    (r_direct-or-not_part_of ~[?e ?x]  r_inverse: r_direct-or-not_part,
      \. (r_KRL ~[Language_element ?le, KRL ?krl]); 
         (r_KRL-set ~[?c ?krls] := [?c r_KRL: (a KRL r_part of: ?krls)]) 
    );


   r_relation_from_description ~[Description_content-or-instrument-or-container, Thing]
    \. (r_relation_from_AE ~[AE, Thing] 
         \. (r_relation_from_document ~[Document_or_reference_to_one, Thing]
              \. r_relation_from_and_to_document //below
                 r_document_version )
            (r_relation_from_structured_value ~[Structured_value, Thing]
              \. (r_relation_from_collection ~[Collection, Thing]
                    \. (r_direct-or-not_member ~[?coll, ?e] = r_member,
                         \. r_direct_member
                         := [or_{ [?coll r_direct_member: ?e],
                                  [?coll r_direct_member: (a Collection
                                                            r_direct-or-not_member: ?e)]} ] )
                       (r_relation_from_list ~[List, Thing] \. r_first r_rest)
                       (r_relation_from_set_of_types ~[{1..* Type}, Thing]
                         \. r_types_intersection )
                 ) )
            r_relation_from_and_to_AE ~[AE, AE]  //below
       );
   
   
   r_relation_to_description ~[Thing, Description_content-or-instrument-or-container]
    \. r_description_container ~[Thing, Description_container]
       r_relation_to_description_content ~[Thing, Description_content]
       (r_relation_to_description_instrument ~[Thing, Description_instrument]
         = r_description_instrument  r_descr_instrument  r_descr_instr,
         \. (r_relation_to_language_element ~[Thing, Language_element]
              \. (r_language_element \. r_representation)
                 (r_relation_to_AE ~[Thing, AE] 
                   \. r_relation_from_and_to_AE //below
                      r_descr ~[Description_content, AE]
                      r_relation_to_type //see end of section
                      (r_relation_to_collection ~[Thing,Collection]
                        \. (r_parts ~[?x,?list] // ^(...): lambda-abstraction (~ owl#Restriction)
                             :/^ [any ^(Thing  r_member of: ?list) r_part of: ?x],
                             :\. [any ^(Thing  r_part of ?x)  r_member of: ?list] )
                           (r_types_intersection_of  r_inverse: r_types_intersection) )
                      (r_relation_to_value_token ~[Thing, Value_token]
                        \. r_value 
                           //r_relation_to_CE //if CEs are seen as values
                      )
                 )
            ) );
   
    r_relation_from_and_to_AE-or-thing_that-should_be ~[Thing, Thing]
      \. (r_relation_from_and_to_AE ~[AE, AE]
           \. (r_relation_from_and_to_document
                  ~[Document_or_reference_to_one, Document_or_reference_to_one]
                \. r_incompatible_document  r_prior_version  r_backward_compatible_document )
              (r_relation_to_AE_part /^ r_part,
                \. (r_reification_relation_to_AE
                     \. exclusion
                        { (r_operator ~[AE, Operator] = r_op,
                             \. r_frame_head ) //~ rdf#predicate
                          (r_argument = r_arg, 
                             \. (r_frame-or-link_argument
                                  \. r_half_link  r_link_source //~ rdf#subject
                                                  r_link_destination //~ rdf#object
                                ) )
                          (r_args ~[AE ?a, List ?l] 
                            :<= [ [?a r_arg: ^arg] <=> [^arg  r_member of: ?l] ] )
                        } ) )
              (r_result ~[AE, AE]
                \. (r_reference_of  ~[Referring_individual_AE, AE]
                      r_inverse: r_reference  ~[AE,Referring_individual_AE] )
                   pm#output  //directly (+ also by reification)
              )
              (r_relation_from_type_to_AE ~[Type, AE]
                \. (r_relation_from_and_to_type ) //see below
         )
         (r_relation_that_is_or_should_be_from_AE_to_CE ~[Thing, Thing]
           \. (r_relation_to_CE ~[Thing, CE]
                \. (r_CE = rc) 
                   (r_name ~[Thing, Value_token] 
                     \. rdfs#label ~[rdfs#Resource, rdfs#Literal]   r_short_name )
                   (r_language-element_to_CE ~[Language_element, CE]
                     \. (r_operator_name ~[Language_element, Value_token]
                          = rc_operator_name,
                          /^ r_name r_operator)
                        r_AE_to_CE ~[AE, CE]
                        r_CE_to_CE ~[CE, CE]  /* see ../o_KRLnotationTop/d_KRLnotationsTop.html */
                   ) )
         ) );


r_relation_from_or_to_type-or-thing_that-should_be ~[Thing,Thing]
 \. (r_relation_from_type-or-thing_that-should_be
      \. (r_relation_from_type ~[Type,Thing]
           \. (r_relation_from_type_to_collection ~[Type,Collection]
                \. r_relation_from_type_to_collection_of_types ~[Type,.{1..* Type@RDF}]
              )
              (r_relation_from_anonymous_concept_type
                \. r_relation_from_anonymous_concept_type_to_concept_type
                   r_relation_from_anonymous_concept_type_to_value-token_type )
         ) )
    (r_relation_from_and_to_type-or-thing_that-should_be
      \. (r_relation_from_and_to_type ~[Type,Type]
           \. (r_disjoint_type \. r_disjoint_concept_type  r_disjoint_relation_type)
              (r_equivalent_type \. r_equivalent_concept_type  r_equivalent_relation_type)
              (r_supertype_or_equal
                \. (r_strict_supertype = "/^",
                     \. r_proper_super_concept-type  ~[Concept_type, Concept_type]
                        r_proper_super_relation-type ~[Relation_type, Relation_type] )
                   (r_super-or-equal_concept-type ~[Concept_type, Concept_type]
                     \. r_proper_super_concept-type )
                   (r_super-or-equal_relation-type ~[Relation_type, Relation_type]
                     \. r_proper_super_relation-type ) )
              (r_relation_from_and_to_concept_type ~[Concept_type, Concept_type]
                \. r_complement_type   r_super-or-equal_concept-type
                   r_disjoint_concept_type  r_equivalent_concept_type
                   r_relation_from_anonymous_concept_type_to_concept_type
                     ~[Anonymous_concept_type, Concept_type]
                   r_relation_from_and_to_value-token_type
                     ~[Value-token_type,Value-token_type]
              )
              (r_relation_from_relation_type_to_type ~[Relation_type, Type]
                \. (r_relation_from_relation_type_to_concept_type
                       ~[Relation_type, Concept_type]
                     \. r_binary-relation-type_domain // \. rdfs#domain
                        r_binary-relation-type_range )// \. rdfs#range
                   (r_relation_from_and_to_relation_type
                     \. r_inverse  r_disjoint_relation_type  r_equivalent_relation_type) )
         )
         (r_relation_to_type-or-thing_that-should_be
           \. (r_relation_to_type ~[Thing, Type]
                \. r_relation_from_and_to_type ~[Type, Type] //above
                   (r_type ~[Thing,Type]
                     \. r_datatype ~[Value_token,Value-token_type]
                        (r_declaration_with_type ~[Constant,Type]
                           r_inverse: r_instance_declaration ),
                     r_inverse: (r_instance \. r_instance_declaration) )
                   (r_part_type ~[Thing ?x, Type ?t] 
                     := [?x  r_part: (a thing r_type: ?t)] ),
                     \. (r_KRL_type_of  r_inverse_relation: r_KRL_type)
                   )
                   (r_relation_from_AE_to_CE_type ~[AE ?ae, CE_Type ?ceType]
                     \. (rc_type ~[AE ?ae, CE_Type ?ceType]  = r_CE_type,
                          := [?ae  r_CE: (a CE  r_type: ?ceType)] )  
                     //people who see CEs as specializations of AEs can also
                     // state:  rc_type /^ r_subtype;   r_CE /^ r_instance;
                   ) )
         ) );
/* One use of the function f_in 
   defined below is to refer to the "specialization in a model" of a type from the
   top-level of KRLO, i.e., a type not related to a particular model. 
   This definition exploits the fact that in KRLO, from any Language_element to a Language,
   there is a chain of part or member relations. 
   In FL, as also defined below, "@" is used as an infix operator for abbreviating the
   use of this function.

  f_in ~[?elemType, ?languageType ] -: ?elemTypeInLanguage
    :- [?elemTypeInLanguage
         = ^(?elemType ?e  r_KRL_type=: ?languageType,
               //and [?e.part /^^ ?elemType] implies [?e.part /^^ ?elemTypeInLanguage]
               r_direct-or-not_part_of_same_type=: a ?elemTypeInLanguage ) ],
    rc_type=: fc_type _(.[fc_ARG_(?elemType) fc_OP_("@") fc_ARG_(?languageType) 
                         ], .{FL});    //thus, ?part@?whole refers to ?type 
*/


/* The function f_destination_of_such_link_from_such_source defined below ("f_dest" in this article)
   permits to refer to the destination of a given binary relation from a given source.
   In FL, as also defined below, "." is used as an infix operator for abbreviating the
   use of this function.

  f_destination_of_such_functional_link_from_such_source
     ~[ ?link_source, ?link_rel_type ] -: ?link_dest 
    := [?link_source  ?link_rel_type: ?link_dest],
    rc_type=: fc_type _(.[fc_ARG_(?link_source) fc_OP_(".") fc_ARG_(?link_rel_type)
                         ], .{FL}); //thus, ?link_source.?link_rel_type refers
                                    //   to ?link_dest_sequence
*/


0.3.  First subtypes of Abstract_element (AE)

0.3.1.   First partitions for AEs

Abstract_element //= AE,  
 \. partition
    { (Phrase /* in Section 0.3.2:  = Reference-to-phrase_or_non-reference_phrase,
        \. partition
           { (NR_phrase = Non-reference_phrase) //see Section 1
             (Reference_to_phrase r_reference of=: 1..* Phrase)
           } */ )  //i.e.:  = ^(Referring_individual_AE r_result: 1 Phrase)
      (AE_that_is_not_a_NR-phrase_nor_a_reference_to_a_phrase
        \. partition { Value_token  Reference_to_something_that_is_not_a_phrase
                       Non-referable_AE_that_is_not_a_NR-phrase_nor_a_value-token } )
    }
    partition 
    { (Value_token  /* see Section 2.3
        = Token_literal Unstructured_value  Atomic_value */ )
      Referring_AE_or_NR-phrase  //see Section 0.3.3
    }
    partition
    { NR_phrase /* e.g., NR-formulas  */
      (Value_or_reference  /* e.g., Terms and Quantifiers; see Section 2 */
        \. partition
           { Value_token //Token_literal  Atomic_value  Unstructured_value
             (AE_that_is_not_a_NR-phrase_nor_a_value-token
                \. partition
                   { Reference-token_or_structured-value_or_type /* see Section 0.3.3 */
                     (Non-referable_AE_that_is_not_a_NR-phrase_nor_a_value-token
                       \. Logical_operator )
                   } )
           }
           partition
           { (AE_that_is_not_a_NR-phrase_nor_a_token 
               = Term_that_is_not_a_token            
                 Expression_that_is_not_a_sentence_nor_a_token,
               \. partition
                  { Structured_value-or-reference_or_type
                    Non-referable_AE_that_is_not_a_NR-phrase_nor_a_value-token
                  } )
             (Token =  Atomic_value-or-reference  Constant_or_variable,
               \. partition { Referring_token/*e.g. Variable*/  Value_token }
                  partition { Variable  Constant } )  //see a bit below
           }
           partition 
           { Reference_to_phrase
             AE_that_is_not_a_NR-phrase_nor_a_reference_to_a_phrase 
           }
           partition 
           { Variable  //quantified name (NCNAME), e.g., blank node name; 
                       //a Name (below) is for a named argument
             (Value_or_referring_AE-that-is-not-a-variable 
               \. partition
                  { (Constant
                      \. partition { Value_token  Identifier } 
                         partition { (Untyped_constant \. Untyped_value_token)
                                     (Typed_constant \. Typed_value_token,
                                       r_operator: 1 Constant_type,
                                       r_arg: 1 Untyped_constant )
                                   } )
                    (Value_or_referring_AE-that-is-not-a-variable-nor-a-constant
                       \. Name  Structured_value-or-reference_or_type )
                  }
                  partition
                  { Function_call 
                    (Value_or_referring_AE_that_is_not_a_variable_nor_a_function_call
                      \.  Constant  Name  Structured_value  Type
                          Structured_referring_AE_that_is_not_a_function_call )
                  } )
           } )
    }
    partition  
    { Token 
      (Non-token_AE 
        \. partition
           { NR_phrase //functions like f_and take bags of phrases as arguments
             Structured_value-or-reference_or_type
           }
           partition
           { (Non-ordered_non-token_AE  \. Set)
             (Ordered_non-token_AE 
               \. partition
                  { (Positional_AE  /^ Positional_language_element,
                      \. Positional_formula  List)
                    (Non-positional_AE
                      \. exclusion
                         { (AE_with_named_arguments
                             /^ Language_element_with_named_arguments,
                             \. (Phrase_with_named_arguments
                                  \. Formula_with_named_arguments ) )
                           (Frame  /^ Frame_element,
                             \. partition {Frame_about_a_phrase  Frame_not_about_a_phrase}
                                partition
                                { (Frame_as_NR-phrase     //rif#Frame in FORMULA
                                    \. partition { Frame_as_NR-phrase_about_a_phrase
                                                   Frame_as_NR-phrase_not_about_a_phrase
                                                 } )
                                  (Frame_as_reference 
                                    /^ ^(Non-token_AE  r_operator: 1 AE),
                                    \. partition
                                       { Frame_as_reference_about_a_phrase  //external or not
                                         Frame_as_reference_not_about_a_phrase
                                       }       
                                       Minimal-frame_as_reference )
                                } )
                         } )
                  } )
            } )
    } 

    partition //KRL specifications specialize Predefined_AE by their own AEs
    { (Non-referable_AE  r_reference of: 0 Referring_individual_AE,
        \. Non-referable_AE_that_is_not_a_NR-phrase_nor_a_value-token )
      (Referable_AE  //1st order entity 
        r_reference: 0..* Referring_individual_AE,
        //e.g., r_variable: 0..* Variable,   r_result of: 1...* Function_call,
        r_annotation: 0..* AE_that_can_be_annotation_value )
                      //if referable then linkable and annotatable
    }
    partition //KRL specifications specialize the next two types by their own AEs
    { AE_that_cannot_be_annotated_without_link
      AE_that_can_be_annotated_without_link  //generally: (all and) only Referable_AE
    }
    partition //KRL specifications specialize the next two types by their own AEs
    { AE_that_cannot_be_annotation_value
      AE_that_can_be_annotation_value  
    }
    partition //KRL specifications specialize the next two types by their own AEs
    { AE_that_cannot_be_a_component
      (AE_that_can_be_a_component
        \. Component_of_an_AE_that_is_not_an_NR-phrase ) //detailed below
    }
    (Grammar_element \.  Phrase_of_a_grammar  Referring_AE_of_a_grammar); 


0.3.2.   Phrase

Phrase = Reference-to-phrase_or_non-reference_phrase, 
  := "Sentence (syntactic/structural abstract statement) or reference to it",
  \. partition
     { (NR_phrase = Non-reference_phrase) /* see Section 1 */
       (Reference_to_phrase r_reference of=: a Phrase)
     }
    %{ (Modularizing_phrase \. Modularizing_NR-phrase)
       (Formula
         \. partition
            { NR_formula  //see Section 1
              (Reference_to_formula  r_result: a Formula)
            }
            (Atomic_formula
              \. partition { NR_atomic_formula  //see Section 1
                             (Reference_to_atomic_formula  r_result: an Atomic_formula)
                           }
                 (Link \. partition { NR_link  //see Section 1
                                      (Reference_to_link  r_result: a Link)
                                    } ) ) )
     }
     partition 
     { (Definition //to define a constant
         \. partition { Non_conservative_definition  Conservative_definition }
            (Type_definition \.  Function_type_definition)
       )
       (Inference_rule        //similar to an implication but its conclusion is 
         \. Production_rule ) //  "true" only if/when the rule is fired
       (Phrase_that_is_not_a_definition_nor_an_Inference_rule //old: = Sentence,
              //no Phrase_that_can_be_asserted since in coop.html this includes Definition
         //fact in a world: formula assigned a truth-value in an interpretation
         \. (Belief \. Observation Preference) //the fact that someone believes in a certain thing
            Axiom  //Phrase assumed to be true, from/by which others are derived
            Proof  Tautologie  Deduced_phrase
       )
     }
     partition
     { (Formula_that_cannot_introduce_an_inconsistency \. Conservative_definition)
       (Formula_that_can_introduce_an_inconsistency
         \. Non_conservative_definition Belief Axiom Inference_rule )
     }
     Command_as_phrase  //as opposed to  Command_as_function_call
     Phrase_of_a_grammar;


0.3.3.   Referring_AE_or_NR-phrase

Referring_AE_or_NR-phrase  //reference or description  
 \. partition { Reference-token_or_structured-value_or_type     //see below
                NR_phrase //see Section 1
              }
    (Phrase
       \. (Document_or_reference_to_one
            \. partition
               { Document
                 (Reference_to_a_document  r_reference of=: 1..* Document_or_reference_to_one)
               } ) )
    (Command
      \. partition
         { Command_as_function_call
           (Command_as_phrase
             \. partition
                { Command-as-phrase_not_modifying_the_KB
                  (Command-as-phrase_modifying_the_KB
                    \. partition
                       { Command-as-phrase_monotically_modifying_the_KB
                         (Command-as-phrase_non-monotically_modifying_the_KB
                           \. Non_conservative_definition )
                       }
                       partition { Statement_assertion  Statement_retraction } )
                }
                (Parsing_directive \. Module_directive) )
         }
         partition 
         { (Command_not_modifying_a_KB = Query,  
             \. partition
                {Command_as_function_call  Command-as-phrase_not_modifying_the_KB} )
           Command-as-phrase_modifying_the_KB 
         }
         exclusion { (Addition \. Statement_assertion)
                     (Removal  \. Statement_retractation)
                   }
    );


    Reference-token_or_structured-value_or_type = Reference  Referring_AE,
      r_reference of=: 1 Thing, 
      \. pm#sbvr#Place_holder
         partition
         { Type  //Section 0.1
           (Referring_individual_AE
             \. partition { Referring_token  Structured_referring_AE } ) // below
         }
         partition  
         { Referring_token  //see below  (this includes Phrase_referring_token)
           (Structured_referring_AE_or_type
             \. partition { Type  Structured_referring_AE } )
         }
         partition
         { (Reference_to_something_that_is_not_a_phrase
             \. Structured_reference_to_something_that_is_not_a_phrase  
                Token_referring_to_something_that_is_not_a_phrase  Type )
           (Reference_to_phrase 
             \. partition { Structured_reference_to_phrase  //defined just above
                            Phrase_referring_token  //defined below
                          } )
         }
         partition
         { (Reference_to_something_that_is_not_a_type
             \. Structured_reference_to_something_that_is_not_a_type  
                Token_referring_to_something_that_is_not_a_type )
           (Reference_to_type    r_result=: 1 Type,  
             \. partition { Structured_reference_to_type  //defined just below
                            Type_referring_token  //defined below
                          } )
           
         };

          Structured_referring_AE = Structured_reference,  r_part =: 1..* AE, 
             \. partition
                { Function_call
                  (Structured_referring_AE_that_is_not_a_function_call
                    \. Frame_as_reference    Structured_value )
                } 
                partition
                { Structured_reference_to_local_AE  //by default
                  (Structured_reference_to_non-local_AE  //when origin made explicit
                    \. exclusion 
                       { (Structured_reference_to_AE_in_a_remote_module //with same KRL
                            \. Structured_reference_to_formula_from_a_remote_module,
                            frame-as-ref_type_("Remote",r_remote_AE,
                                               .[1 AE, 1 Remote-module_reference] ) )
                         (Structured_reference_to_externally_defined_AE  //another KRL
                            \. Structured_reference_to_externally_defined_formula,
                            /^ frame-as-ref_type_("External",r_external_reference,
                                                  .[1 AE, 1 Module_locator] ) )
                       } )
                }
                partition
                { (Structured_reference_to_phrase   r_result=: 1 Phrase,
                    \. exclusion
                       { Function_call_returning_a_phrase  Frame_as_reference_about_a_phrase
                         Structured_value_referring_to_a_phrase //e.g., an Or-collection
                         Structured_reference_to_formula_from_a_remote_module
                         Structured_reference_to_externally_defined_formula
                       }
                       (Structured_reference_to_formula r_result: 1 Formula,
                         \. (Structured_reference_to_atomic_formula
                              r_result: 1 Atomic_formula ) )
                  )
                  (Structured_reference_to_something_that_is_not_a_phrase
                    \. exclusion
                       { Function_call_not_returning_a_phrase
                         Frame_as_reference_not_about_a_phrase
                         Structured_value_not_referring_to_a_phrase
                       } )
                }
                partition
                { (Structured_reference_to_type   r_result=: 1 Type)
                  (Structured_reference_to_something_that_is_not_a_type r_result=: 0 Type)
                };


         Referring_token = Atomic_reference,
          \. partition
             { (Variable //cl#Sequence_marquer; quantified NCNAME), e.g., blank node name;
                 \. partition                     //a Name (below) is for a named argument 
                    { (Variable_referring_to_a_phrase
                         = ^(Variable r_result: 1 Phrase))
                      (Variable_not_referring_to_a_phrase
                        \. Variable_not_referring_to_a_relation_type_nor_to_a_phrase )
                    }
                    partition
                    { (Variable_referring_to_a_relation_type
                        = ^(Variable r_result: 1 Relation_type) ),
                      (Variable_not_referring_to_a_relation_type
                        \. Variable_not_referring_to_a_relation_type_nor_to_a_phrase )
                    }
                    partition
                    { Free_variable
                      (Bound_variable
                        \. partition
                           { Explicitly_bound_variable
                             (Implicitly_bound_variable
                               \. exclusion
                                  { Implicitly_existentially_bound_variable
                                    (Implicitly_universally_bound_variable
                                      \. partition
                                         { (Implicitly-universally-bound_sequence-variable
                                             = kif#sequence_marker  cl#sequence_marker )
                                           Implicitly-universally-bound_non-sequence-variable
                                         }
                                         exclusion
                                         { Definition_argument_variable  
                                           (Aggregate_variable
                                             \. partition { Comprehension_variable
                                                            Grouping_variable } )
                                         
                                         } )
                                  } )
                           } )
                    } )
               (Identifier_or_name //atomic or not
                 = Referring_token_that_is_not_a_variable,
                 \. partition
                    { Name  //e.g., a Named_argument
                      (Identifier
                        \. partition
                           { (Absolute_identifier 
                               \. partition
                                  { (Local_absolute_identifier
                                      \. partition
                                         { IRI_with_local_namespace  //"..."^^rif:local
                                           (Blank_node_identifier 
                                             \. Sparql_blank-node_ID //'_' NCName
                                         } )
                                    (Non-local_absolute_identifier \. Absolute_IRI)
                                  }
                                  (IRI \. IRI_with_local_namespace  Absolute_IRI)
                                  Module_locator /*for referring to external AEs */ )
                             Relative_identifier 
                           }
                           partition
                           { Phrase_identifier 
                             (Identifier_not_referring_to_a_phrase \. Symbol_space)
                           }
                           (Module_reference /*for referring to AEs in remote modules */
                             \. Remote-module_reference ) 
                           Symbol_space )
                    }
                    partition
                    { Identifier_or_name_not_referring_to_a_phrase
                      (Identifier_or_name_referring_to_a_phrase /^ Reference_to_phrase,
                        \. (Identifier_referring_to_a_document /^ Reference_to_a_document,
                              (Document_IRI /^ IRI) ) )
                    }
               )
             }
             partition
             { (Phrase_referring_token = ^(Token r_result: 1 Phrase),
                 \. Formula_referring_token = ^(Token r_result: 1 Formula),
                    partition
                    { Variable_referring_to_a_phrase
                      (Identifier_or_name_referring_to_a_phrase \. Phrase_identifier,
                        \. (Identifier_or_name_referring_to_a_formula  ) )
                    } )
               (Token_referring_to_something_that_is_not_a_phrase
                 \. partition { Variable_not_referring_to_a_phrase
                                (Identifier_or_name_not_referring_to_a_phrase
                                  \. Identifier_not_referring_to_a_phrase )
                              } )
             }; 


0.4.  Functions for easing the use of relation types from Section 0.2




 //a Link is an AE for a binary relation, hence a reified binary relation, like an rdf#Statement
f_link ~[?operator_name, ?binary-rel_type, ?link_source, ?link_destination]
            =: the Link ?l
   := [?l  r_AE of: [(?binary-rel_source r_descr: ?link_source)
                     ?binary-rel_type: (?binary-rel_destination r_descr: ?link_destination)
                    ] ?r,
           r_operator_name: ?operator_name,       r_result: ?r, 
           r_operator: (?link_type  r_descr of: ?binary-rel_type),
           rdf#predicate: ?binary-rel_type, 
           r_link_source: ?link_source,  r_link_destination: ?link_destination
      ];

f_link_type ~[?operator_name, ?r_binary-rel_type,
                   ?link-type_domain, ?link-type_range ] =: the AE_type ?lt
   := [any ?lt = f_link _(?operator_name, ?r_binary-rel_type,
                          1 ?link-rel-type_domain, 1 link-type_range )];


f_relation ~[?operator_name, ?rel_type, ?arg_list] =: the Formula ?rr
   := [?rr  r_AE of: [ ?rel_type _(?%args)] ?r,  r_operator_name: ?operator_name,
            r_operator: ?rel_type,  r_args: ?arg_list,  r_result: ?r ];

f_relation_type  ~[?operator_name, ?rel_type, ?arg_list] =: the AE_type ?pt
   := [any ?pt = f_relation _(?operator_name,?rel_type,?arg_list) ];



f_frame_as_ref ~[?operator_name, ?binary-rel_type, ?link_destination]
                    =: the Frame_as_reference ?f
   := [?f /^^ Frame_as_reference,
        r_result: f_link_(?operator_name, ?binary-rel_type, ?f,
                          ?link_destination ) ];

f_frame-as-ref_type ~[?operator_name, ?r_binary-rel_type,
                           ?link-type_domain, ?link-type_range ] =: the AE_type ?lt
   := [any ?lt = f_link_ref _(?operator_name, ?r_binary-rel_type,
                              1 ?link-rel-type_domain, 1 link-type_range )];


f_function_call ~[?parameter-name_type, ?fct_type,
                       ?arg_list_with_named_parameter_or_not ] =: the Function_type ?rf
   := [?rf  r_AE of: [^res = ?fct_type _(%?arg_list_with_named_parameter_or_not)
                     ] ?f,
            r_operator: ?fct_type, r_args: ?arg_list_with_named_parameter_or_not,
            r_result: ^res ];

f_function-call_type ~[?parameter-name_type,?fct_type,?arg_list] =: the AE_type ?ft
   := [any ?ft = f_function _(?operator_name,?fct_type,?arg_list) ];


f_quantification ~[?operator_name, ?quantifier_type, ?guard-types-AEs,
                        ?variable_list, ?formula_body] =: the Phrase ?p
   := [?p  r_AE of: [ ?quantifier_type _(?guard-types-AEs ?variable_list ?formula_body)
                    ] ?r,
           r_operator_name: ?operator_name,  r_operator: ?quantifier_type, 
           r_args: (1 Quantification_argument_list 
                        r_operator: ?formula_body,  
                        r_args: (1 Quantification_variable_argument_list
                                  r_operator: ?variable_list, r_args: ?guard_list ) ),
           r_result: ?r ];

                     
f_quantification_type ~[?operator_name, ?quantifier_type, ?guard_list,
                             ?variable_type, ?formula_body] =: the AE_type ?qt
   := [any ?qt = f_quantification _(?operator_name,?quantifier_type, ?guard_list,
                                    .[1..* ?variable_type], ?formula_body) ];



1.  NR_phrase (or component of it)     (figure)

In this section, non-bold italic characters are used names coming from (i.e., inspired by) RIF-FLD (the links to RIF types are in another file). Bold characters are for easing understanding.

NR_phrase = r_relation ~[ %[1..* AE] ?%aes ], 
  = ^(NR_term r_operator: 1 ^(Type /^ NR_phrase), 
              r_result: 1 (Truth_value \.. True False Indeterminate_truth-value) ),
  \. Modularizing_NR-phrase  NR_formula; 


Phrase_component \. { Modularizing_phrase_component  Non-modularizing_phrase_component };


1.1.  Modularizing_NR-phrase

Modularizing_NR-phrase
  \. partition 
     { (Group_of_phrases /^ f_relation_type _("",r_and,.[0..* Phrase]),
         \. (Module_or_module-list  //cl#NamedText cl#Module
              \. (Module = f_link_type _("",r_context,Module_body,Module_context)
                   \. (Module_with_a_name = ^(Module ?m  r_part: f_link_("Name",r_name,?m,n)))
                     %{ (Module_that_may_have_submodules r_link_source=: 0..1 Or{Module,Formula})
                        (Module_that_may_not_have_submodules r_link_source=: 0 Formula)
                      } )  
                 (Module_list =  /^ f_relation_type _("",r_and,.[0..* Module]))
                 (Document  //head element of a KRL grammar ; cl#Text
                   \. Ontology )
            (Module_context /^ f_relation_type _("Context",r_and,.[0..* Link_in_module_context]))
            (Module_body  /^ f_relation_type _("Group",r_and,.[0..* Formula])) 
        
       (Modularizing_group-of-phrases_part
         \. (Link_in_module_context
              \. partition
                 { (Link_from-or-to_a_module_body 
                     \. (Link_to_a_module_body  r_link_destination: a Module_body)
                        (Link_from_a_module_body  r_link_source: a Module_body,
                          \. (Module_version_link ?l
                                := [?l=f_link_("",r_document_version,?l.r_link_source,IRI)] )
                             (Module_IRI_link ?l
                                := [?l=f_link_("",r_identifier,?l.r_link_source,IRI)] )
                             (Module_annotation_link ?l  /^ Annotation_link,
                                := [?l=f_link_("",r_annotation,?l.r_link_source,
                                               AE_that_can_be_annotation_value )] 
                             )
                             (Remote_module_naming_link ?l
                                := [?l=f_link_("",r_remote_module_naming, ?l.r_link_source,
                                               .[1 Referring_individual_AE, 1 Module_locator] )] )
                             (Module_name_link ?l
                                := [?l=f_link_("Name",r_name,?l.r_link_source,Name)] )
                             (Module_dialect_link ?l
                                := [?l=f_link_("Dialect",r_dialect,?l.r_link_source,Dialect)] )
                             (Module_base_IRI_link ?l
                                := [?l=f_link_("Base",r_base_IRI,?l.r_link_source,IRI)] )
                             (Module_context_namespace-definition_link ?l  //link to 1 link/def.
                                := [?l=f_link_("Prefix",r_namespace_definition,?l.r_link_source,
                                               Namespace_shortcut_definition_in_context )] )
                             (Module_context_type-definition_link  //link to 1 frame on 1 rel. type
                                := [?l=f_link_("",r_relation-type_definition,?l.r_link_source,
                                               Relation-type_definition_in_context )] )
                             (Module_excluded_AE_link ?l
                                := [?l=f_link_("",r_excluded_AEs,?l.r_link_source,Excluded_AEs)] )
                             (Module_import_link ?l
                                \. (Module_import_link_with_IRI ?l
                                     := [?l=f_link_("",r_module_import,?l.r_link_source,IRIp)] )
                                   (Module_import_link_with_locator and_profile ?l   
                                     := [?l=f_link_("",r_module_import,?l.r_link_source,
                                                   .[1 Module_locator, 0..1 Importation_profile] )] )
                             )
                             (Module_domain_restriction_link ?l
                                := [?l=f_link_("",r_domain_restriction, ?l.r_link_source,
                                               1 Referring_individual_AE )] )
                        ) )
                   (Link_from-or-to_a_distributive_set_of_elements_of_a_module_body 
                     \. (Link_from_each_concept_and_relation_of_a_module_body ?l
                          r_link_source=: %{each ^(Node r_member of: a Module_body)} ) 
                   )
                 } ) )
     };


Modularizing_phrase_component 
  \. Importation_profile
     (Namespace_shortcut_definition_in_context /^ f_link_type _("",r_shortcut,Name,Identifier))
     (Relation-type_definition_in_context  /^ Frame_as_NR-phrase, //on 1 rel. type
        r_frame_head: 1 Relation_type ?r,
        r_args: .[0..* ^(Half-link_in_rel-type-def_in_context  r_link_source: ?r)] )
     (Half-link_in_rel-type-def_in_context /^ Half-link,
       \. (Minimal_half-link_in_rel-type-def_context /^ Minimal_half-link,
            \. (Minimal_half-link_in_rel-type-destination-def_context@JM ?mh
                 r_frame_head: r_binary-relation-type_range ) ) )
     (Excluded_AEs = .[0..* AE])
     Local_universe; 

r_relation_from_modularizing_NR-phrase ~[Modularizing_NR-phrase,*]
 \. (r_relation_for_module_context
      \. r_context ~[Module_body,Module_context]    r_dialect ~[Module_body,Dialect]
         r_base_IRI ~[Module_body,IRI]              r_shortcut ~[Name,Identifier] 
         r_namespace_definition ~[Module_body,Namespace_shortcut_definition_in_context]
         r_remote_module_naming ~[Module_body,.[1 Referring_individual_AE, 1 Module_locator]]
         r_module_import ~[Module_body,.[1 Module_locator, 0..1 Importation_profile]]
         r_domain_restriction ~[Module_body, Local_universe]
    );


1.2.  NR_formula

NR_formula 
 \. partition 
    { (Positional_formula  r_arg: 1..* Type)
      (Non-positional_formula
        \. exclusion
           { (NR_formula_with_named_arguments  r_arg: 1..* Named_argument)
             Frame_as_NR-phrase
           } )     
    }
    partition
    { NR-formula_in_local_module
      (NR-formula_not_in_local_module
        \. exclusion
           { Remote_NR-formula  
             Externally_defined_NR-formula 
           } )
    }
    partition_if _([Logical_operator r_exclusion: r_relation]) 
    { (Composite_formula  = f_relation_type _("",Logical_operator,.[1..* Formula]),
        \. partition  
           { (Connective_formula  r_operator: 1 ^(Type /^ Connective_operator),
               \. partition { Negative_formula  Positive_formula }
                  exclusion
                  { (Connective_formula_with_1_argument
                      = f_relation_type_("",r_unary_relation,.[1 Formula]),
                      \. (Negative_formula
                           \. exclusion
                              { (Symmetric_negating_formula
                                   = f_relation_type_("Not",r_not,.[1 Formula]) )
                                (Negation-as-failure_formula
                                   = f_relation_type_("Naf",r_naf,.[1 Formula]) )
                              } )
                         (Constraint = f_relation_type_(":-",r_constraint,.[1 Formula])
                           <=> f_Link_type_(":-",r_rule-implication_of,False_formula,Formula) )
                    )
                    (Connective_formula_with_2_arguments
                      = f_Link_type_("",r_binary_relation,Formula,Formula),
                      \. (Rule = f_Link_type_(":-",r_rule-implication_of,(Rule_premise /^ Formula),
                                              (Rule_conclusion /^ Formula) ),
                           \. exclusion
                              { (Inference_rule \. Production_rule) //as defined above
                                (Logical_rule /^ Phrase,
                                  \. (Logical_implication
                                       r_operator: 1 ^(Type /^ r_implication),
                                       \. (Logical_equivalence = biconditional) ) )
                              }
                              exclusion{ (Implication_only \. Production_rule)
                                         (Logical_equivalence
                                            r_operator: 1 ^(Type /^ r_equivalent_phrase))
                                       }
                         ) )
                    (Connective_formula_with_variable_number_of_arguments
                      = Variable-n-ary_connective_phrase
                        f_relation_type_("",r_variable-ary_relation,.[1..* Formula]),
                      \. exclusion
                         { (Disjunction_of_formulas = f_relation_type_("Or",r_or,.[1..* Formula]))
                           (Conjunction_of_formulas = f_relation_type_("And",r_and,.[1..* Formula]),
                             \. (Conjunction_of_existential_formulas 
                                   = f_relation_type_("And",r_and,
                                                      .[1..* Existentially_quantified_formula] ) )
                                (Conjunction_of_atomic_formulas 
                                   = f_relation_type_("And",r_and,.[1..* Atomic_formula]) )
                                (Conjunction_of_links
                                  =  f_relation_type_("And",r_and,.[1..* Link]),
                                  \. Frame_as_conjunction_of_links_from_a_same_source ) )
                         }
                         (Connective_phrase_on_atomic_formulas  r_arg: 1..* Atomic_formula,
                           \. Conjunction_of_atomic_formulas )
                    )
                  } )
             (Quantified_formula 
                = f_quantification_type _("",Quantifier,.[0..1 Type],Referring_token,Formula),
                \. (Classic_quantified_formula
                     = f_quantification_type_("",Quantifier,.[],.[1 Variable],Formula) ) 
                   (First-order_logic_quantified_formula
                     = f_quantification_type_("",Quantifier,.[0..1 Type],
                                   Token_referring_to_something_that_is_not_a_phrase,Formula ) )
                   exclusion 
                   { (Universally_quantified_formula
                       = f_quantification_type_("Forall",q_forall,.[0..1 Type],
                                                Referring_token,Formula ),
                       \. (Classic_universally_quantified_formula
                            = f_quantification_type_("Forall",q_forall,.[],Variable,Formula) ) )
                     (Existentially_quantified_formula
                       = f_quantification_type_("Exists",q_exists,.[0..1 Type],
                                                Referring_token,Formula ),
                       \. (Classic_existentially_quantified_formula
                            = f_quantification_type_("Exists",q_exists,.[],Variable,Formula) ) )
                   } )
           } )
      (NR_atomic_formula
        \. partition 
           { (Non_frame_NR_atomic_formula = Formula_with_only_one_relation,
               = f_relation_type _("",r_relation,.[1..* AE]) 
               \. partition
                  { (Relation_on_at_least_one_statement
                      = f_relation_type _("",r_relation,.[1..* Phrase, 0..* AE]) )
                    Relation_not_on_a_statement
                  }
                  (NR_link ?l = Link_as_positional_formula,  /^ Positional_formula,
                     /^ f_link_type _("",r_binary_relation,Type,Type),
                     rdf#predicate: a binary-relation_type ?rt,
                     r_link_source: a Concept_node ?source,
                     r_link_destination: a Concept_node ?dest,
                     <=> ^(Frame_as_NR-phrase ?f  r_frame_head: ?source, r_arg: ?l),
                     \. (Type_link = f_link_type _("#",r_type,AE,Type) )
                        (Supertype-or-equal_link
                          = f_link_type_("##",r_supertype-or-equal,Type,Type),
                          \. (Supertype-or-equal_link_to_anonymous_type
                               \. f_link_type_("##",r_supertype-or-equal,Type,Anonymous_type) )
                             (Proper_supertype_link
                               = f_link_type_("/^",r_strict_supertype,Type,Type) )
                             (Equal_link = f_link_type _("=",r_equal,AE,AE) ) )
                        (Annotation_link = f_link_type _("",r_annotation,AE,
                                                            AE_that_can_be_annotation_value))
                  ) ) 
             (Frame_as_NR-phrase ?f 
               <=> ^(Frame_as_conjunction_of_links_from_a_same_source ?f2
                       r_frame_head: 1 Concept_node ?fh,
                       r_arg: 1..* ^(NR_link  r_link_source: ?fh)  )
               := [?f  r_frame_head: ?fh,
                       r_args: .[0..* ^(Half-link  r_link_source: ?fh)] ?l,
                       r_result: ?f,
                       = [ ?fh /^^ ^(Frame_as_reference  r_result: ?fh,
                                       r_frame_head: ?fh, r_args: ?l ) ]
                  ], 
               \. (Minimal-frame_as_NR-phrase  
                    = [?f  r_frame_head: ?fh,
                           r_args: .[0..* ^(Minimal_half-link  r_link_source: ?fh)] ?l,
                           r_result: ?f,
                           = [?fh /^^ (Minimal-frame_as_reference  r_frame_head: ?fh,
                                                                   r_args: ?l, r_result: ?fh) ]
                      ] ) )
           } )
    };


Non-modularizing_phrase_component
  \. (Named_argument  r_operator: 1 Type, r_arg: 1 Name) 
     (Concept_node  r_operator: 1 Type,  r_arg: 0..1 Cardinality,
        \. (Minimal_concept_node  r_arg: 0 AE) )
     (Half_link  
        r_operator: 1 ^(Type /^ r_binary_relation), 
        r_link_source: 1 Concept_node,
        r_link_destination: 1..* Concept_node, 
        \. (Minimal_half-link  r_operator: 1 ^(Type /^ r_binary_relation),
                               r_link_destination: 1 Minimal_concept_node ) )
     (Quantification_guard_list  /^ .[0..* Type] )  
     (Quantification_variable_list  /^ .[1..* Referring_token])
     (Quantification_variable_argument_list
        r_operator: 1 Quantification_variable_list, r_arg: 0..1 Quantification_guard_list )
     (Quantification_argument_list
        r_operator: 1 ?formula_body,  r_arg: 1 Quantification_variable_argument_list );



2.  Value (structured or not) or reference (to a phrase or not)


2.1.  Operator (function type, ...)

/* Reminder: 
Operator //= cl#operator, /^ Type, //AE and Type_as_description_content
  \. Function_type  Relation_type  Logical_operator_type; 
     //Relations and logical operator are not necessarily exclusive in some HOLs  */


Logical_operator /^^ Logical_operator_type,  
          \. partition
             { (Quantifier
                 \. exclusion{ (Universal_quantifier = q_forall)
                               (Existential_quantifier = q_exists)
                             } 
                    Cardinality //quantifier for a destination node
               )
               (Connective_operator 
                 \. exclusion
                    { (One-ary_connective_operator
                        \. (Negation_operator \. (r_not \. rif#neg) (r_naf \. rif#naf)) )
                      (Two-ary_connective_operator  \. r_implication)
                      (Variable-Nary_connective_operator
                        \. (And_connective = r_and)  (Or_connective = r_or) )
                    } )
               (Aggregation-function_or_list_operator
                 \. f_list  //function that returns a list
                    (Aggregation-function_operator 
                      \. (f_min = rif#Min) (f_max = rif#Max) (f_sum = rif#Sum) (f_prod = rif#Prod)
                         (f_count = rif#Count) (f_avg = rif#Avg) 
                         (f_set = rif#Set) (f_bag = rif#Bag) ) )
             }; 


Function_call  = ^(Non-token_AE r_operator: 1 Function_type),
  \. partition
     { (Non-aggregate_function_call = Expression)
       (Aggregate_function_call 
         \. ( Aggregate_function 
                 r_operator:  1 ^(Type /^ Aggregation-function_operator),
                 r_arg: 1 Aggregate_function_argument_list ) )
     }
     Lambda_expression  Function_call_returning_a_phrase 
     Command_as_function_call; 

Function_component
  \. (Aggregate_function_component
       \. (Aggregate_function_bound_list
             r_operator:  1 Comprehension_variable, r_arg: 0..* Grouping_variable )
          (Aggregate_function_argument_list
             r_operator: 1 Formula,  r_arg: 1 Aggregate_function_bound_list )
     );//e.g.:  count{?Stud[?Crs]|Exists ?Semester (u:takes(?Stud ?Crs ?Semester))})))
       //       avg  {?Sal[?Dept]|Exists ?Empl u:salary(?Empl ?Dept ?Sal)}                 


2.2.  Structured Value

Structured_value  //kind of Frame_as_reference for partOf links
  /^ ^(Non-token_AE r_operator: 1 AE) 
  \. Collection;
     partition
     { (Structured_value_not_referring_to_a_phrase
         \. Collection_not_referring_to_a_phrase )
       (Structured_value_referring_to_a_phrase
         \. Collection_referring_to_a_phrase ) //e.g., an Or-collection
     };

Collection
  \. partition
     { Collection_not_referring_to_a_phrase
       (Collection_referring_to_a_phrase
         \. And-collection  Or-collection )
     }
     partition
     { (Collection_without_possible_element_redundancies = Set, 
         \. (Set_organised_by_a_partial_order_relation  \.  Tree  Lattice)
            Set_organised_by_a_full_order_relation
            (Set_of_nodes_and_arcs = Graph  
              \. (Set_of_nodes_and_n-ary-arcs = Hypergraph)
                 (Set_of_nodes_and_oriented_binary-arcs = Oriented_graph)
                 (Set_of_nodes_connected_by-arcs = Connected_graph) )
            (Set_of_phrases \. rdf#Alt)
       )
       (Collection_with_possible_element_redundancies = Bag,
         \. (Sequentially-accessible_bag = List  Sequence, 
              \. partition             
                 { (Closed_list = f_collection_type _("List",.[1..* Closed_list_member]))
                   (Open_list = f_collection_type _("List",.[1..* Closed_list_member,
                                                                  1 Open_list_sequence_variable] ))
                 }                   
                 exclusion { (LIFO_list = Stack)  (FIFO_list = Queue) }
                 sumo#Unique_list (^list which happens to have no redundancies^) 
                 List_with_one_element
                 (Null_list = kif#nil) 
                 List_of_alternatives //\. rdf#Seq
                 (List_playing_a_role 
                   \. (cl#Term_sequence = .[1..* cl#term_or_sequence_marquer],
                        \. cl#Argument_sequence ) ),
              \.. Null_list ) // = kif#nil rdf#nil
            (Index-accessible_bag
              \. (Bag_indexed_by_integers = Array,
                   \. exclusion { Static_array  (Dynamic_array = Vector) }
                      (Array_part_of_an_array \. Column (Row \. Head_row) ) 
                 )
                 (Bag_indexed_by_objects_that_are_not_integers
                   \. (Dynamic_bag-indexed-by-objects-that-are-not-integers 
                        = Associative_array,
                        \. (Associative_array_via_hash_function = Hash_table  Hash_map)
                      )     //this last data type is type of concrete data structure
                      (Bag_indexed_by_strings = Object,
                        \. partition
                           { (Static_object = Record)
                             (Dynamic_object = Dictionnary)
                           } )
                      (Array_of_array = Table, part: 1..* Array_part_of_an_array) )
            )
            (Collection-with-possible-element-redundancies_stored_on_a_permanent_memory = File)
       )
     }
     (Recursive_data_structure \. List  Tree  Lattice  Graph)
     (rdfs#Container \. exclusion{ rdf#Bag  rdf#Alt rdf#Seq })
     Lexical-grammar_character-set
     (Collection_of_phrases  \. Set_of_phrases  Bag_of_phrase)
     (Collection_of_types  r_member=: 1..* Type,
       \. (Disjoint_types ?ts
            r_member=: 1..* ^(Type  r_disjoint_type: any ^(Type != ?t, r_member of: ?ts)) )
          (Equivalent_types ?ts
            r_member=: 1..* ^(Type  r_equivalent_type: any ^(Type != ?t, r_member of: ?ts)) )
          (Same_things ?ts
            r_member=: 1..* ^(Thing  =  any ^(Type != ?t, r_member of: ?ts)) )
          (Different_things ?ts
            r_member=: 1..* ^(Thing  != any ^(Type != ?t, r_member of: ?ts)) )
     );


Component_of_an_AE_that_is_not_an_NR-phrase  /* /^ AE_that_can_be_a_component, //already done */
 \. Phrase_component
    (Structured_value_component
      \. (List_member \. partition { Closed_list_member  Open_list_sequence_variable }) )
    (Structured_referring_AE_component
      \. Function_component );


2.3.  Value token

Value_token ?vt = Token_literal  Atomic_value  Unstructured_value,
                     = rdfs#Literal,  /^^ rdfs#Datatype,   //not done when RDF is represented
   := [a token ?t r_result: ?t],
   /^ ^(AE  r_part =: 0 Abstract_element)  //aka "terminal (token)"
      ^(Value_or_reference ?vor r_result =: ?vt), 
   \. partition { Structured_value_token  Atomic_value_token }
      partition
      { Untyped_value_token //obsolete: rdf#PlainLiteral
        Typed_value_token 
      }
      partition { Unordered_value_token
                  (At_least_partially_ordered_value_token
                    \. Time_value_token  Real_number Imaginary_number  Complex_number
                       (Totally_ordered_value_token \. Integer) )
                }
      (Value_token_encoded_in_a_certain_base  \. xs#base64Binary  xs#hexBinary)
      Language-tagged_string_value //= rdf:langString 
      CE;


Structured_value_token
  \. (String_value_token = rdf#PlainLiteral,
       \. partition //xs: http://www.w3.org/2001/XMLSchema http://www.w3.org/TR/owl-ref/#rdf-datatype
          { (String_without_language_tag = xs#string,
              \. xs#normalizedString )
            (String_with_language_tag  r_operator: 1 xs#language, r_arg: 1 xs#string )
          } 
     )
     (Time_value_token  //partially ordered
       \. partition
          { (Point-in-time_value_token
              \. xs#date  (xs#dateTime \. xs#dateTimeStamp) xs#time )
            (Duration_value_token 
              \. xs#dayTimeDuration xs#yearMonthDuration )
          }
     );
       

Atomic_value_token
 \. Not_a_number
    (Boolean = xs#boolean, \. (True = xs#true kif#true)  (False = xs#false kif#false))
    (Character
      \. (Unicode_character  
           \. (w3c#Char \. #x9 #xA #xD %[- #x20-#xD7FF] %[- #xE000-#xFFFD] %[- #x10000-#x10FFFF]) )
         (Space_character = w3c#ECHAR, = f_character_type_(.{" ","\t","\n","\r","\b","\f"}))
         (Digit = Arabic_digit, = f_character_type _(.[- '0'-'9'])) //= partition { %[- '0'-'9'] }
         (Letter = Un-accentuated_latin_character,
           \. partition
              { (Uppercase_un-accentuated_latin_character = f_character_type _(.[- 'A'-'Z']))
                (Lowercase_un-accentuated_latin_character = f_character_type _(.[- 'a'-'z']))
              } )
         (Hexa_character = f_character_type _( .{ Arabic_digit  %[- 'A'-'F']  %[- 'a'-'f'] }))
    )
    (Number 
      \. exclusion
         { (Complex_number  part= .{Real_number Imaginary_number})
           (Real_number (^number that can be expressed as a (finite or not) decimal^)
             \. partition
                { Irrational_number  
                  (Rational_number (^product of dividing two integers^)
                    \. (Integer (^a negative or nonnegative whole number^),
                         \. partition
                            { (xs#nonNegativeInteger = kif#natural xs#unsignedInt,
                                \. partition {xs#positiveInteger  kif#zero}
                                   (NonNegativeInteger_with_a_size_limit
                                     \. xs#unsignedLong  xs#unsignedShort xs#unsignedByte ) )
                              xs#negativeInteger
                            }
                            partition
                            { (xs#nonPositiveInteger 
                                \. partition {xs#negative_integer  kif#zero} )
                              xs#positiveInteger
                            }
                            partition
                            { (Integer_with_a_size_limit \. xs#int  xs#long  xs#short  xs#byte
                                                            NonNegativeInteger_with_a_size_limit )
                              (Integer_without_a_size_limit
                                \. xs#positiveInteger  xs#nonNegativeInteger
                                   xs#nonPositiveInteger  xs#negativeInteger )
                            }
                            (Integer_encoded_in_a_certain_base \. xsd#decimal)
                            partition {Even_integer  Odd_integer} 
                            Prime_number ) )
                }
                partition
                { (NonNegative_real_number
                    \. partition { (Positive_real_number \. Positive_integer)
                                   kif#zero } )
                  (Negative_real_number \. Negative_integer)
                }
                partition
                { (Real_number_with_a_size_limit  
                    \. (Floating_point_real_with_a_size_limit \. xs#double xs#float)
                       Integer_with_a_size_limit )
                  (Real_number_without_size_limit  \. xs#precisionDecimal)
                } 
                (Real_number_encoded_in_a_certain_base
                  \.  xs#decimal  xs#precisionDecimal  Binary_number )
                Imaginary_number )
         }
    );