_You can enter a room once, yet leave it twice. — Peter Landin_
Kontynuacja reprezentuje "resztę obliczeń" w danym punkcie wykonania programu.
W językach funkcyjnych, kontynuacje dostępne są albo bezpośrednio, przy użyciu
tzw. stylu przekazywania kontynuacji (continuation-passing style, CPS), albo
pośrednio, przy użyciu tzw. operatorów sterowania (np. call-with-current-
continuation w języku Scheme). Kontynuacje znajdują szereg zastosowań zarówno
teoretycznych, m. in. w semantyce denotacyjnej i izomorfizmie Curry'ego-
Howarda dla logiki klasycznej, jak również praktycznych, takich jak
programowanie z nawrotami, programowanie współbieżne czy kompilacja języków
funkcyjnych.
W ramach seminarium prezentowane będą zarówno klasyczne jak i najnowsze prace
dotyczące teorii i zastosowań kontynuacji. W szczególności, przyjrzymy się
własnościom rachunku lambda rozszerzonego o operatory sterowania, poznamy
metody transformowania programów z kontynuacjami, a także zastanowimy się nad
obliczeniową interpretacją logiki klasycznej oraz związkami rachunku sekwentów
z maszynami abstrakcyjnymi. Spróbujemy też dowiedzieć się jakie twierdzenie
logiki klasycznej i jaki program jest przedmiotem następującej historii,
opowiedzianej przez Phila Wadlera na konferencji ICFP w 2003 roku:
_Once upon a time, the devil approached a man and made_ _an offer: “Either (a)
I will give you one billion dollars, or (b)_ _I will grant you any wish if you
pay me one billion dollars._ _Of course, I get to choose whether I offer (a)
or (b).” The man was wary. Did he need to sign over his soul?_ _No, said the
devil, all the man need do is accept the offer._
_The man pondered. If he was offered (b) it was unlikely_ _that he would ever
be able to buy the wish, but what was_ _the harm in having the opportunity
available? “I accept,” said the man at last. “Do I get (a) or (b)?” The devil
paused. “I choose (b).” The man was disappointed but not surprised. That was_
_that, he thought. But the offer gnawed at him. Imagine_ _what he could do
with his wish! Many years passed, and_ _the man began to accumulate money. To
get the money he_ _sometimes did bad things, and dimly he realized that this_
_must be what the devil had in mind. Eventually he had his_ _billion dollars,
and the devil appeared again._
_“Here is a billion dollars,” said the man, handing over a_ _valise containing
the money. “Grant me my wish!” The devil took possession of the valise. Then
he said,_ _“Oh, did I say (b) before? I’m so sorry. I meant (a). It is_ _my
great pleasure to give you one billion dollars.” And the devil handed back to
the man the same valise_ _that the man had just handed to him._
Na drugim końcu spektrum zagadnień, o ile znajdą się bardziej praktycznie
zorientowani uczestnicy seminarium, mogą zostać omówione najnowsze
zastosowania stylu przekazywania kontynuacji oraz operatorów sterowania w
takich językach jak JavaScript i Ruby.
**Literatura (orientacyjna):**
1. Andrzej Filinski. Representing Monads. POPL 1994.
2. Olivier Danvy, Andrzej Filinski. Abstracting Control. LISP and Functional Programming 1990.
3. Olivier Danvy, Andrzej Filinski. Representing Control: A Study of the CPS Transformation. Mathematical Structures in Computer Science 2(4): 361-391 (1992).
4. Zena M. Ariola, Hugo Herbelin, Amr Sabry. A type-theoretic foundation of delimited continuations. Higher-Order and Symbolic Computation 22(3): 233-273 (2009).
5. Zena M. Ariola, Aaron Bohannon, Amr Sabry. Sequent calculi and abstract machines. ACM Trans. Program. Lang. Syst. 31(4): 13:1-13:48 (2009).
6. Zena M. Ariola, Hugo Herbelin. Control reduction theories: the benefit of structural substitution. J. Funct. Program. 18(3): 373-419 (2008).
7. Zena M. Ariola, Hugo Herbelin, Amr Sabry. A proof-theoretic foundation of abortive continuations. Higher-Order and Symbolic Computation 20(4): 403-429 (2007).
8. Paul Downen, Zena M. Ariola: Compositional semantics for composable continuations: from abortive to delimited control. ICFP 2014.
9. Pierre-Louis Curien, Hugo Herbelin. The duality of computation. ICFP 2000.
10. Philip Wadler. Call-by-value is dual to call-by-name. ICFP 2003.
11. Timothy Griffin. A Formulae-as-Types Notion of Control. POPL 1990.
12. Michel Parigot. Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. LPAR 1992.
13. Matthias Felleisen, Robert Hieb: The Revised Report on the Syntactic Theories of Sequential Control and State. Theor. Comput. Sci. 103(2): 235-271 (1992).
14. Paul Downen, Zena M. Ariola: A tutorial on computational classical logic and the sequent calculus. J. Funct. Program. 28: e3 (2018)
15. Andrew Kennedy: Compiling with continuations, continued. ICFP 2007: 177-190
