Abstrakt. Vi definierar ett begrepp av normal form tvåsimilaritet för otypade call-by- value λ-calculus utvidgas med de avgränsade kontroll operatörer skifta och återställa. Normal form tvåsimilariteter är enkla, lättanvända beteende ekvivalenser som relaterar termer utan att behöva testa dem i alla sammanhang (som kontextuell ekvivalens), eller genom att tillämpa dem på funktionsargument (som applicativ bisimilaritet). Vi bevisar att den normala formen tvåsidighet för skift och återställning är ljud men inte komplett w.r.t. Sammanhangsmässig likvärdighet och vi definierar upp till tekniker som syftar till att förenkla bisimuleringsbevis. Slutligen illustrerar vi enkelheten i de tekniker vi utvecklar genom att bevisa flera ekvivalenser på villkor.
I ett tidigare arbete REF definierar vi extensional enf bisimilarities och bisimulations upp till sammanhang för en call-by- value λ-calculus med avgränsade kontrolloperatörer.
Normal Form Bisimulations for Delimited-Control Operators
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Computer Science']}