A formal "behaves identically" equivalence between two systems: each can match the other's observable steps. Used to prove that compiling MeTTa to Rholang preserves behavior.

← Back to the Glossary