 Total Modal: A category of rewrite rules that must always have more terms in the left-hand side, than on the right-hand side. When found to be the only type of rules in a program, it makes up for a non-turing complete program that will always terminate. For example, where "swap" is the fuel: <> (swap ?x ?y) (?y ?x) 5 comments
@isagel yeah, in the case where a rewrite rule takes more terms than it writes, it's part of the terminating category :) this isn't super clear to me! it seems like balancing on the boundary of completeness. it seems like this argument is pretty well tied to the evaluation of modal, no? if you have more thoughts about how this fits into the chomsky hierarchy, i'd love to hear about it, but this is plenty of motivation for me to play with modal :> |
Gregory's Server
@neauoire It is my goal in life to one day understand your posts about Modal~