search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
451 stars 149 forks source link

Disambiguate the notion of `function` in Kore #3326

Open ana-pantilie opened 1 year ago

ana-pantilie commented 1 year ago

The work being done to migrate the Haskell backend to deprecate the usage of the functional attribute has revealed a problem with our terminology: the function attribute has two distinct meanings.

  1. We use the constructor and the function attribute to distinguish between two separate categories of symbols.
  2. The ML meaning of function (or function-like) is that a symbol application constructs patterns which preserve the property of being semantically interpreted as a singleton set or the empty set.

The two notions are problematic because 2. applies to constructor symbols as well, therefore we cannot use 1. to distinguish between the two categories of symbols.

Proposal

My suggestion would be, in the spirit of modernizing Kore, to remove the second meaning from the Kore language:

  1. function will only be added to symbols which are not constructors, they are symbols which are provided an equational rewrite theory
  2. constructor symbols will not be marked as function (or total) since they are already regarded to be function-like and not bottom in the ML sense.
amelieled commented 1 year ago

I'm not sure to understand the problem here, because for me, 2. doesn't make sense in the current Kore because there is no applicative operator.

ehildenb commented 1 year ago

What does Frontend should generate function, total for total functions and constructor for constructors mean? Are we already adding constructor attribute for free constructors with no equational axioms? Are there exampples we are missing?