K-user mailing list

[<isaacdefrain AT gmail.com>]

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.