Reflective algorithms are algorithms that can modify their own behaviour. Recently a behavioural theory of reflective algorithms has been developed, which shows that they are captured by reflective abstract state machines (rASMs). Reflective ASMs exploit extended states that include an updatable representation of the ASM signature and rules to be executed by the machine in that state. Updates to the representation of ASM signatures and rules are realised by means of a sophisticated tree algebra defined in the background of the rASM. In this paper the theory is taken further by an extension of the logic of ASMs to capture inferences on rASMs. The key is the introduction of terms that are interpreted by ASM rules stored in some location. We show that fragments of the logic with a fixed bound on the number of steps preserve completeness, whereas the full run-logic for rASMs becomes incomplete.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{ScheweF20,
author = {Klaus{-}Dieter Schewe and
Flavio Ferrarotti},
editor = {Alexander Raschke and
Dominique M{\'{e}}ry and
Frank Houdek},
title = {A Logic for Reflective ASMs},
booktitle = {Rigorous State-Based Methods - 7th International Conference, {ABZ}
2020, Ulm, Germany, May 27-29, 2020, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12071},
pages = {93--106},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-48077-6\_7},
doi = {10.1007/978-3-030-48077-6\_7},
timestamp = {Mon, 25 May 2020 12:33:39 +0200},
biburl = {https://dblp.org/rec/conf/asm/ScheweF20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}