pristine:0000001363-a3bac700027a7d7457fbaabc040e274c57d1946ecee5ad22addaca131ac4da85 [Started formalising "What is the meaning of these constant interruptions?". Nils Anders Danielsson **20080429020036] hash: 0000019863-197d29d403c1c0854c334ad226ecaae1959a7f98fb89ef0c4866cf9897bd9055 [Added a boring file. Nils Anders Danielsson **20080429020114] hash: 0000000189-26e9ef94036ea20fd355a68dbc9dcf5788c890ed9a00e8c0918ad04b49785b65 [Defined the virtual machine and compiler. Nils Anders Danielsson **20080429115533] hash: 0000003969-ace566f18114b1398250533fd4f5df36391367f18d88e53e220ba3689a75b9e8 [Proved completeness. Nils Anders Danielsson **20080429115545] hash: 0000003079-d1146bc13ca12a3346ab3d5fe27da1e0b96d49728fab3d15106ef74e61f2c25d [Identified a problem in the paper. Nils Anders Danielsson **20080429140758] hash: 0000001671-14f678249eacb242df8690c82f4374835663941e6e0611d7734b80640a273935 [Proved soundness. Nils Anders Danielsson **20080429173350] hash: 0000009160-ac24210fa037d5a588665c3b90ee8ef7dc62d4e4a8832ba5f91632d04ba7aa4a [Updated code to reflect changes in library API. Nils Anders Danielsson **20080430222517] hash: 0000010128-80b0b81307767067b7d3865872afecc9d9ad1825efd2ecfd1a5c48762b23b92c [Proved that ⊕ is associative. Nils Anders Danielsson **20080501180110] hash: 0000002034-2cd7cfabec3fca491aa5b28f5e7d88458251738386506cba7685b3f5a8fc03fc [Examined if _⊕_ is commutative. Nils Anders Danielsson **20080501182645] hash: 0000001380-e8cec42db79ceb0bab5d45440a32ff47b8e402edb1820242c28301dffdf42ec3 [Updated code to reflect changes in library API. Nils Anders Danielsson **20080519142359] hash: 0000000342-aca69d89c38f14a1b8eb8347d24f65e4d1d71fe7b72d1fd417c4cfb14259e858 [Renamed _⇑[_] to _↯[_]. Nils Anders Danielsson **20080519142756] hash: 0000015514-c356936f598bf6c1bf59ea32969cd36f63498f6af6ce755ba04a5c05144bc992 [Formatting. Nils Anders Danielsson **20080519151951] hash: 0000000581-775daf00c1dfffa7342a375768a9b178241e49c5e5c6273df79601a5ea0fdd14 [Added a small-step semantics, equivalent to the big-step one. Nils Anders Danielsson **20080520194255] hash: 0000010936-6e9a9f989a3c449667c70c5474265f8d060657aeacad20c15ba063428097ebcd [Changed to a more obviously correct formulation of compiler correctness. Nils Anders Danielsson **20080520194822 + Rebranded (a specialisation of) the old soundness statement as part of completeness. + Proved that the old soundness statement implies the new one. ] hash: 0000030314-2a6f49e7383cb763e978b0359ae446bbf34821ad3bdf7752957e782c0af8cfc9 [Tried adding an infinitely looping construct. Nils Anders Danielsson **20080521194124 + This code is unfinished. + I decided to include non-termination as one of the results of the big-step semantics. However, this seems to be a bad idea, for two reasons: 1) With a more complicated language it won't be possible to include non-termination in the inductive big-step relation. 2) Non-termination requires special treatment in many results anyway, so breaking out non-termination into a separate relation will (probably) be a simplification. ] hash: 0000050298-2fa55a3c7194c963790155afe8295171428ad4bf8b7ff4f3ac9b030660b1b692 [Noted that the small-step semantics is incorrect. Nils Anders Danielsson **20080522231008 + With respect to the big-step semantics; it allows an infinite sequence of interrupts. ] hash: 0000000560-36f63de05c538f8a28008395852b0f3049b757dc087cc727b8a3af6269f84a9d [Tried another approach to non-termination. Nils Anders Danielsson **20080610155140 + A separate big-step relation now encodes non-termination. This approach seems more promising, but some proofs are still unfinished. There are two main problems: 1) The inductive encoding of infinite transition sequences that I am using is quite awkward to work with. A coinductive encoding would probably be more natural. Fortunately Agda has recently (after I wrote most of the code in this patch) gained support for coinductive definitions. 2) The bar theorem does not imply soundness any more, since all I can prove now is that terms /which are guaranteed to terminate/ will reach some final state when run in the VM, and then the bar lemma does not apply. However, it may be possible to prove soundness directly by using the small-step semantics instead of the big-step one. ] hash: 0000077122-7b886bf82dfa86518a0885e31a2d1534fabd870982bd7c90b58366ca907364a0 [Changed to a coinductive definition of infinite transition sequences. Nils Anders Danielsson **20080610160001] hash: 0000001356-72512e5d9d48f64b90af9569b0481f4911e0a7ecc6aca2de4f637f966cd00bd5 [Made the big-step non-termination relation coinductive. Nils Anders Danielsson **20080610201238] hash: 0000004646-07b23f494721c2c88d49c0a952560a778be7e9c9137c44191e4e3626e910c4a6 [Changed the semantics: Interrupts are now blocked upon entry to the handler. Nils Anders Danielsson **20080612213401 + This seems more reasonable, since it avoids a race condition. It is also consistent with GHC. + Updated most parts of the code. The new small-step semantics has not been proved equivalent to the big-step one yet, though. I'll try to simplify the semantics in order to make this proof easier. (Currently the semantics uses expressions which are annotated with interrupt status at (basically) every internal position.) ] hash: 0000052180-5273b07dff659462981297d0e61b978ea9d39a8de78c58395f7015126fe4cec9 [Tried to simplify the small-step semantics. Nils Anders Danielsson **20080612215911 + This variant only allows interrupts at redex positions. Infinite sequences of interrupts are not possible, since interrupts are immediately taken care of by the innermost exception handler (if any). + However, the presence of such non-small steps has an unwanted effect: the lift⟶ lemma is not valid. I think that it can be awkward to work with a semantics without this lemma. ] hash: 0000016181-4b93aae8a950481a66b395421b97ae905172e7c7ba72a086f8b077bd37566264 [Updated code to reflect changes in library API. Nils Anders Danielsson **20080615100502] hash: 0000000601-ca7d3e05ce1d63926af290156041437ac679aebf68d5e108f9e900fe20c4c0ae [Removed an unnecessary part of the compiler correctness statement. Nils Anders Danielsson **20080616170052] hash: 0000001971-2a4c8748c1e02f3b8c5b0419a007d11bd1491f1b359c94556729b4c9fc92bbed [Added a characterisation of infinite reduction sequences. Nils Anders Danielsson **20080617145207] hash: 0000006194-875c1f7f97a13fe6fb52265391014b303363bd9ce8e6240d46566883480f3acd [Improved the small-step semantics. Nils Anders Danielsson **20080618114042 + I have now almost managed to prove that the small- and big-step semantics are equivalent. However, it seems as if I need a slightly smarter setup in order to make the last component of the proof productive. ] hash: 0000044186-922ed6dbba5e9c43bc3a42a89635c918d13db7e4b135ed94a2daea916a08bf3a [Split up the ⇑ relation into an inductive and a coinductive part. Nils Anders Danielsson **20080618115512 + I thought that this could perhaps make some proofs easier, since inductive types are easier to work with than coinductive types. However, I have not seen any evidence that this is actually the case, and furthermore the mixed inductive/coinductive definition is probably harder to understand than the other one, so I will revert this patch. ] hash: 0000012176-4fbdc4adc41af6844a5d6b12b71a43f0e72d337c2bee48f916adb304a491657a [Split up the ⇑ relation into an inductive and a coinductive part. Nils Anders Danielsson *-20080618115512 + I thought that this could perhaps make some proofs easier, since inductive types are easier to work with than coinductive types. However, I have not seen any evidence that this is actually the case, and furthermore the mixed inductive/coinductive definition is probably harder to understand than the other one, so I will revert this patch. ] hash: 0000012176-c7c5eb0031db926bef1663f43576962a67aba2a99603cdeb8901e7ffb3d44037 [A failed attempt at proving small⇒big⟶∞ without using excluded middle. Nils Anders Danielsson **20080618144219] hash: 0000002367-e239dd48d3bf2d687058ae120d6aefa5ce87212d8d3fb017ca76c4595e874395 [Added _◁∞_. Nils Anders Danielsson **20080624132911] hash: 0000004036-d6155c8acb33f08403fc8ed33dca984dcc4f13dfc69d75051279ca689c9d5442 [Added bounded-is-finite. Nils Anders Danielsson **20080624132930] hash: 0000000377-4aecfb26f3cf512732cd77d1870689ba01e389905e9e7fbf7485824e8f6805e7 [Made the bar theorem useful by switching from _◁_ to _◁∞_. Nils Anders Danielsson **20080624132947] hash: 0000024080-8947260d9dfb56b13baa9f29ac1e4da9d19c889e617ac7f2079496edbe9bed3c [Added possibly infinite sequences. Nils Anders Danielsson **20080624135134] hash: 0000003393-ce3795dc7149b22428519c4435477b6db2c7edf0751262c78a434a486d40d2d9 [Added unbounded-loops. Nils Anders Danielsson **20080624135201] hash: 0000000746-cfb8a513d36058ba95241cfe7419722e9cb1c352f83d4cea33651ec1eb89d729 [Added a representation of infinite sequences as functions from ℕ. Nils Anders Danielsson **20080624135251] hash: 0000001401-095507aec5ca0fcd9db25d085c7373a64e41b245236621384e0e57ccd563acf6 [Renamed _∘_ to _⊚_. Nils Anders Danielsson **20080624135340] hash: 0000002721-6a0dc0a24c7a2f7192551673f513b12543d135f4cf59cb2abd63e03b0f81f71c [Proved some lemmas about run and done. Nils Anders Danielsson **20080624135648] hash: 0000002894-fd973524f7e0ec4b646ca7d21865ca4f02e633d814735469f5f880ee7c17efac [Defined _⟶⋆∞[_]_. Nils Anders Danielsson **20080624135710] hash: 0000000408-4e13e898441fa016e04000dbe09fc5f3a41339e21978855b3625e259a46470bd [Found a way to finish the equivalence proof. Nils Anders Danielsson **20080624151447 + I reformulated the correctness statement using double negation. + The proof is not finished yet. In an attempt to reduce tedium in the remaining cases I plan to stop using evaluation contexts in the definition of the small-step reduction relation. ] hash: 0000009438-ce9c210f3ccf0f370c421ea56ec3fc5bf378e267a5efef2ad217703422ffab4d [Evaluation contexts are no longer used to define the small-step semantics. Nils Anders Danielsson **20080624185631 + They are still used by some of the proofs, though. ] hash: 0000031820-5a4961a44295c93eaef304f0e97446f2f1dff8808f466f23aae0c34a55af6a20 [Finished the equivalence proof. Nils Anders Danielsson **20080624193150] hash: 0000010938-9b2e9f93bd2009e34de63b5677a452a8d1afb1191cb42f4c79ec6cacbeddcc5b [Brought some code up to date. Nils Anders Danielsson **20080624194108] hash: 0000001957-b142240ec8a791c668846aef09f6da2665eb8f646b6632c63533e409e7db710d [Simplified some things by replacing the constructors val and throw with ⌜_⌝. Nils Anders Danielsson **20080624201229] hash: 0000031091-b97c904a00b3dc9f453b87d02d7f8680cfa4d4b2819734e538c75be02c09cdc4 [Made loop take an argument. Nils Anders Danielsson **20080626114103 + This makes some proofs more realistic. + Note that some proofs now fail to pass the productivity checker. They are productive, though (as far as I can tell). ] hash: 0000025648-e39572d7a6c3d7adb5893d5596b04286875aca0360898f6bbac11a899dbb1b0d [Made big⇒small⇑ pass the productivity checker. Nils Anders Danielsson **20080703174354] hash: 0000007681-2f28ac04e9d86e6e2988e7a1321b8daaf8393db8e675fe02e5bf4595dfa6a4ad [Made the return constructor superfluous by switching from data to codata. Nils Anders Danielsson **20080703174446] hash: 0000001669-796f8372340a70be27f3fcdc8cb52e26c29c3a8da0d16dfeae00c5fa9d274754 [Made complete⇑ pass the productivity checker. Nils Anders Danielsson **20080717150944 + The technique used for big⇒small⇑ was hard to adapt for complete⇑, so another technique was used instead. This technique feels more like a hack, but appears to be easier to use. ] hash: 0000004587-f5c9468e91484ea1270bac596a9b0f3b56e739197d8a5dbfaa402574ee5346a9 [Stopped using continuation-passing style in the proof of the bar theorem. Nils Anders Danielsson **20080717200813] hash: 0000021797-b4e514c72b0c250bb7b4c133a2de996a8f4aebd044dfc3d1b8cc3dfc9323eab9 [Simplified the method used to make complete⇑ pass the productivity checker. Nils Anders Danielsson **20080717224141] hash: 0000004956-27e94c4cf9b7aa235edb25a23ad59b43940cd3d61da9b27b6c6c6a5a620c1a7f [Made the bar theorem pass the productivity checker. Nils Anders Danielsson **20080717224930] hash: 0000009415-e1898122acfefd13f8e6ec28578b9d7a65a772a4f300c4c25ee8f4f35cf33f89 [Simplified the method used to make bar-thm pass the productivity checker. Nils Anders Danielsson **20080717231227 + It is now very similar to the method used by complete⇑. ] hash: 0000012556-ba78da8cbecb9d1bada8f0084f6ba8275d2e9acc9474447772a2388adfc1d2d8 [Attempted to use "the method" also for big⇒small⇑. Nils Anders Danielsson **20080717234942 + However, lack of inlining before productivity checking made this less appealing than for bar-thm and complete⇑. ] hash: 0000002426-19165f5e484708ebbe61f833e18f8acf77840e9083d6e2a5d444ce7b460b496a [Updated code to reflect changes in library API. Nils Anders Danielsson **20080818170647] hash: 0000000366-9374f8150da1387199ab18b376b5bce505c0aeb9ed5cab1d752abe02209c44f4 [Updated code to reflect changes in library API. Nils Anders Danielsson **20081030131223] hash: 0000001391-0db3c21710d65df509f0d10b28240821d934a2d5846385a9c21f59000344dd5b [Replaced a function with uses of \(). Nils Anders Danielsson **20081030134236] hash: 0000000817-a51282b41fb3e9cef7274e529b63b7dfaeb93418fe6ac02d7a5885002245ff75 [Parameterised the compiler correctness statement on the source semantics. Nils Anders Danielsson **20081103094831 + Placed the current (partial) compiler correctness proof, which uses the big-step semantics, under Semantics.BigStep. ] hash: 0000005424-eacc1dc8f707e8569d8924df37ceaaebe6bd91e8b98bb2aa7de42027907c4f1c [Updated code to reflect changes in library API. Nils Anders Danielsson **20081103104539] hash: 0000001145-c600bc341992febc7fcac53d7fea30a46c8794f967247fec300900cb691961f8 [Proved some lemmas related to MaybeInfinite. Nils Anders Danielsson **20081103141429] hash: 0000003840-13545e02d5d08d3a15fc8869c3c724005d61ae4e15dd4649c9dfe0230f846317 [Named a constructor argument. Nils Anders Danielsson **20081103141440] hash: 0000000217-e3d2c20c7c8b846c7498f6b6e0f095942ea313f86ed1ce3241028e526cc8d090 [Almost proved the remaining compiler correctness statement. Nils Anders Danielsson **20081103142234 + By going via the small-step semantics. + It does not quite seem to be possible to prove the key lemma without using double-negation, so I decided to document the current state of the proof. Double-negation seems to be needed because the virtual machine accepts interrupts more often than the small-step semantics. However, a better fix might be to change one of the semantics (or both) so that they become more similar. ] hash: 0000009877-769b2e9b614651a3c3096abad2968ed1795aa4438eb2457d8af6c494128cc32c [Removed StepGroups, which was not very useful. Nils Anders Danielsson **20081103152022 + And which would not have survived the next patch unchanged. ] hash: 0000006319-25d86bed53c4c2297bfc98742a4e366c74265dad84911e387b6cdd1a3ed3e03c [Tweaked the small-step semantics; finished the compiler correctness proof. Nils Anders Danielsson **20081103152504 + The tweak is to enable interrupts more often. + The small-step semantics is still equivalent to the big-step one. ] hash: 0000005271-12a0612ab28f6bf81bd6adf60e0730e3ea601507578b0db08c9055adfb35d5f1 [Improved some comments. Nils Anders Danielsson **20081104140940] hash: 0000000376-328186718e677291496a34082659fac0797590e67b0eff6ff98af6136ffda494 [Attempted to prove completeness using the small-step semantics. Nils Anders Danielsson **20081104164041 + However, this proof appears to require considerably more work than the proof which uses the big-step semantics, so I have decided to abort this proof attempt. ] hash: 0000005632-c6e4d51f01a81af339057825a7333b7ac729f2eb1689c68ebb718371a6186394 [Tried to make the soundness proof more readable. Nils Anders Danielsson **20081104185206 + By making fewer arguments hidden. ] hash: 0000015242-fb08c172c033d03c26841bf7217bf198f0bf2b3cee6dc6810e60a210870a1b7f [Proved the remaining soundness statement for the small-step semantics. Nils Anders Danielsson **20081104185719 + The proof is (currently) rather ugly, but it is straightforward, and thus it may be easier to come up with than the corresponding proof for the big-step semantics (which uses the bar theorem). ] hash: 0000031332-f1f40472ffad3049d64c6ee7d3aa08b998bb72d17d91a47b1690b54c66ca20ef [Renamed a module. Nils Anders Danielsson **20081104190031] hash: 0000000480-88e66f1b64a8a158ebc4f330ad2e5ce100e0ce7bc91892e55c8a9f91a38b1a3b [Simplified (?) small⇒big⟶∞ by using the double-negation monad. Nils Anders Danielsson **20081107182008] hash: 0000004861-17b9174769f1689d09941a629d08b199bfff03fdc29aa961a646d78932d53308 [Simplified small⇒big⟶∞ further. Nils Anders Danielsson **20081107214133] hash: 0000013870-c5696350718bf36d866b390159d33d6b4f733fee859166e12619de00e816a264 [Added _⋢_. Nils Anders Danielsson **20090105204244] hash: 0000000240-9ba147fc84dbe9ea8fe6518cf41207f1285ec4839a0204cd53030ef5c6034bc5 [Updated code to reflect changes in library API. Nils Anders Danielsson **20090105204322] hash: 0000000355-54d5b646cefe7f91c694c76dd9727ea56972e545c9921da386054ae3c75b2b7d [Fixed comment. Nils Anders Danielsson **20090106150001] hash: 0000000771-372905bcdf4877fd4ecc195f2f4a957d01adec72f239b83b819f46b08dec9307 [Modified layout. Nils Anders Danielsson **20090106164151] hash: 0000000986-dd909db5b38b5ffb6ad4f03ca87f27a395b20841d1054d54627f0a02e08397f8 [Improved the compiler correctness statement. Nils Anders Danielsson **20090106172209] hash: 0000016230-e644841f03f5e6befa31a219e1f3962508999ad7379ecef869c16f51ab93e4f6 [Named some constructor arguments. Nils Anders Danielsson **20090106172854] hash: 0000002157-9ba85339c7ea609c87c8bbb326d64b40e9ca0fc43861ce12f11b6796bbb6ceff [Switched from (forall, ->, \) to (∀, →, λ). Nils Anders Danielsson **20090106174125] hash: 0000087003-8dcbd2065568a965733f64ea350aac969ae5dbecfb1bd5d25c0f922d968a3111 [Generalised some results. Nils Anders Danielsson **20090106183321] hash: 0000003972-1ff563b06a7c34cd49b16a1378b2d62b1921c72f1459450583cd1036015d8285 [Minor simplifications. Nils Anders Danielsson **20090106183349] hash: 0000000440-46747735e32c5f12532fb8974cd61ac046ba9f9b17f1c723877158e8986aac20 [Replaced many uses of ~ with =. Nils Anders Danielsson **20090106191029] hash: 0000024467-d0d25747c4a895879bdffd2c0409e3dcedfbda9d7d20f4ec8c119ac42f0bbed6 [Renamed directly to now and via to later. Nils Anders Danielsson **20090106191305] hash: 0000013533-3763223ee582e3e91c7e429e61416bdd40c90d4178bd5cf25896e458e5720bdc