Up Next
Go up to 2 Proposals for changes to the syntax
Go forward to 2.2 More general application terms

2.1 Introduction of types instead of sorts

A new syntactic category TYPE should be defined 
  TYPE ::= SORT | FUNCTION-TYPE
and at several places, e.g. in predicate types, variable declarations and sorted terms, TYPE should be used instead of SORT: 
  PRED-DECL ::= pred-type TYPE* 
  VAR-DECL ::= var-decl VAR+ TYPE
  SORTED-TERM ::= sorted-term TERM TYPE

For FUNCTION-TYPE there are several possibilities. It could be 

  FUNCTION-TYPE ::=  function-type TOTALITY TYPE* TYPE
or 
  FUNCTION-TYPE ::=  function-type TOTALITY TYPE+ TYPE
In the latter case 
  FUNCTION-DECL ::= function-decl FUNCTION-NAME+ FUNCTION-TYPE
should be replaced with 
  VALUE-DECL ::= value-decl VALUE-NAME+ TYPE
The first of these two proposals support the view that one can declare functions, and constants are just special cases of functions. The second proposal supports the view that one can declare values, which are all constants of a type, which is either a basic sort or a function type. The second proposal has the advantage over the first proposal that it is more uniform in allowing declarations of the form c : t not only for functional types t, but also for basic sorts t. On the other hand it has the disadvantage that it does not allow declarations of partial constants, so it is not an extension of full CASL.
CoFI Note: L-2 --Version 1.0-- 10 April 1997.
Comments to ah@it.dtu.dk

Up Next