Complexity

Notion

• Effort required to understand
• Techniques
  • Limit symbol use
  • Limit function nesting
• Examples
  • Comprehensible:

    ! [X,Y] :
      ( ( homomorphism(X)
        & homomorphism(Y) )
     => homomorphism(compose(X,Y)) ) 

  • Less comprehensible:

    ! [F,A] : 
      ( maps(F,A,A)
     => ( ( one_to_one(F,A,A)
          & inverse_predicate(F,F,A,A) )
      <=> identity(compose_function(F,F,A,A,A),A) ) ) 

Implementation

• Limit the combined number of predicate and function symbols
• Calls the JJParser API to get symbol information
• Low symbol count is good