Crisp Computing

Click here to go to the tool

A FLUS specification is a plain text file containing only two directives:

• sorts
• ops

Each directive is followed by a list of elements between curly brackets, {}, and separated by commas. A sort is identified only by a label. The label must begin with a lower case letter. For instance, nat may concern the "natural numbers", float or quo a limited version of the real numbers, and so on. There is no limit on the number of sorts that you can provide. An operation is defined with a label (that must begin with a lower case letter) followed by a colon (:), and the specification of its sort. The sort of an operation has two parts: the sorts of the parameters and the sort returned. The sorts of the parameters has to be separated by asterisks (*), and before the returned sort the symbol -> must be placed. An operation can have arity=0, in which case it is a constant. For instance, zero: -> nat is the operation that takes no parameter and returns a natural number (which is 0 itself). Example: This example is provided in Section FLUS Tool:

sorts{nat}
ops{zero:->nat, succ:nat->nat}

It has only one sort: nat (the natural numbers), and two operations: a constant, zero, and succ which takes a natural number and returns another natural number (its succesor). This specification implements the Peano definition for natural numbers.

In its current state of developement, FLUS is able to represent a summary of both level 1 and level 3, given a specification (see Specification Grammar to check the grammar of the specifications), which is, the list of sorts, operations and terms. Since some of these sets may be infinite, FLUS computes only elements until a certain degree of deep, given by the user (usually, 3). The complexity of computing each set for each level is highly related to the chosen depth, so it is not recommended to raise it. In the following we list the set of commands that the FLUS tool can perform (as in FLUS Tool):

• Level 1: This command aggregates the outputs of Sorts 1, Ops 1 and Terms 1
• Sorts 1: Returns the set of sorts defined by the user in level 1 (directive sorts). Its complexity class is O(S), where S is the constant number of sorts
• Ops 1: Returns the set of operations defined by the user in level 1 (directive ops). Its complexity class is O(P), where P is the constant number of operations
• Terms 1: Returns valid ground terms in level 1. Its complexity class is O((PA)^D), where D is the chosen Depth and A is the maximum arity.
  Additionaly, it is possible to filter terms by sort: write a certain sort (i.e., nat) in the next textbox, and FLUS will return only terms of that sort.
• Check 1: Checks whether a certain (ground) term, written in the textbox (i.e. succ(zero)) is a valid term in level 1
• Level 3: This command aggregates the outputs of Sorts 3, Ops 3 and Terms 3
• Sorts 3: Returns the set of sorts in level 3. Its complexity class is O(2^DS^D)
• Ops 3: Returns the set of operations in level 3. Its complexity class is O(P)
• Terms 3: Returns valid terms in level 3. Its complexity class is O((PA)^2D).
• Check 3: Checks whether a certain term, written in the textbox (i.e. app(\\_1^succ,\\_0^zero)) is a valid term in level 3 (note the double slashes)

Note the high complexity of the last command (Terms 3), that is O((PA)^2D). This means that the tool may lock if the length of the problem is high.

Some possible specifications are listed below:

Peano naturals

sorts{nat}
ops{zero:->nat, succ:nat->nat}

Peano integers

sorts{int}
ops{zero:->int, succ:int->int, pre:int->int}

Many sorts

sorts{nat, int}
ops{zero:->nat,
      up:nat->int, down:int->nat,
      succ:nat->nat, pre:int->int}

2-arity operation

sorts{int, quo}
ops{zero:->int,
      up:int->quo, down:quo->int,
      succ:int->int, div:quo*quo->quo}