K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

Not in any general capacity. K functions are expected to be only called on functions for which they are defined, similar to pattern matching expressions in any other functional language.

With that being said, you can always define a generic fallback implementation for any particular function very easily:

```

rule func(...) => something() [owise]

```

You can also refer to the arguments of the function when determining the behavior you want:

```

rule func(A, B, C) => something(A, B, C) [owise]

```

On Tue, May 21, 2019 at 5:00 PM <isaacdefrain AT gmail.com> wrote:

Hello,

I have been using K framework for the past several months to define the formal
semantics of Rholang for the RChain project.

I have defined many functions/predicates, i.e. productions with [function]
attribute, which are executed as checks for different properties. Before
embarking on the journey of defining an entire structural type system and type
inclusion predicate, I am wondering if there is any scheme in K for
identifying when a function does not return a result and handling that
situation separately from when it does return a result; e.g. during the
function execution, it tries to compute an argument that has no rule
associated with it, maybe it's defined on Int but has not rewrite rule
associated with a prime input. Is there a general way to detect a situation
like this and instead of just halting the computation, handle it in another
way?

Thank you in advance.

--

Dwight Guth

Director of Engineering

Email: dwight.guth AT runtimeverification.com