Guest User

Untitled

a guest
Dec 11th, 2017
68
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 10.81 KB | None | 0 0
  1. We thank the reviewers for their work on our article and their
  2. detailed feedback.
  3.  
  4. We wish to first address the two main points raised by the reviewers:
  5.  
  6. A. The (informal and technical) meaning of the main result, the Full
  7. Abstraction theorem for the embedding of U into UL.
  8.  
  9. B. The choice of paper structure given the page limits (and in
  10. particular the question of what presentation would make sense in
  11. absence of appendices).
  12.  
  13. Then we will comment on some more local points raised by the review --
  14. feel free to skip this latter part.
  15.  
  16.  
  17. # Main questions
  18.  
  19. A) The Full Abstraction result
  20.  
  21. We made the mistake of using the "short" notation of equivalences, (e
  22. \simeq e'), used when the context and types are evident from the usage
  23. context, in Definition 1 and Definition 2, and the "long" notation of
  24. equivalences, (Gamma |- e \simeq e' : sigma), in Theorem 2. Theorem
  25. 2 is meant to state that if (e, e') are equivalent in the sense of
  26. Definition 1, then they are also equivalent in the sense of Definition
  27. 2. We thank reviewer 1 for noticing this unnecessary confusion, and
  28. will change the article to consistently use the long notation. Below
  29. is a longer explanation of the result of Theorem 1 -- feel free to
  30. skip it if the question was only on a notational level.
  31.  
  32.  
  33. Suppose a user is writing a fragment of program in U as part of
  34. a complete UL program. For example, maybe some of the library
  35. functions that they are calling are actually implemented in L (through
  36. a UL(..) boundary); library functions formally correspond to "free
  37. variables" in an open program. Suppose also that the user performs
  38. equational reasoning on their program fragment (for example, wondering
  39. if a given refactoring is correct) by thinking about
  40. indistinguishability: two fragments are "equivalent" if there is no
  41. way to use them in a program and observe a difference between the
  42. two. Finally, suppose that the user is only thinking about
  43. indistinguishability in U (maybe they do not actually know L). Then,
  44. our Full Abstraction theorem states that the equational reasoning they
  45. perform is in fact valid in the whole program UL: if they conclude
  46. that two fragments are equivalent as U terms (without thinking about
  47. L), they remain equivalent as UL terms. In other words, adding L code
  48. (reimplementing functions in L instead of U, for example) cannot break
  49. the expectations of U users -- in terms of equational reasoning at
  50. least.
  51.  
  52. ¹: it is also the case that if two U terms are *distinguishable* as
  53. U programs (inequivalent), then they are distinguishable in UL. This
  54. is a much simpler result, coming from the fact that the execution
  55. behavior of pure-U programs is unchanged in UL -- a direct property of
  56. the way UL was constructed.
  57.  
  58. "Indistinguishability", that is contextual equivalence, of U program
  59. fragments is formally defined with respect to whole-programs in U and
  60. in UL in Definitions 1 and 2 (we elaborate on these definitions below
  61. in our specific response to Review 1), and the theorem formally states
  62. that contextual equivalence in U implies contextual equivalent in UL.
  63.  
  64. Note that "adding L to U preserves equational reasoning" may seem like
  65. a very limited formal statement (what about other forms of
  66. reasoning?), but that in our experience working with Full Abstraction
  67. in other contexts, it actually captures a lot of other "expectation
  68. preservation" properties that we don't know very well how to state
  69. formally -- a lot of the expectations that users have regarding
  70. program behaviors can be rephrased as equivalence quizzes "are the
  71. fragments X and Y indistinguishable?".
  72.  
  73.  
  74. B) The structure of the paper
  75.  
  76. We have indeed found it challenging to present our work in the page
  77. limits requested for Fossacs submissions. It is not clear to us how
  78. much of the responsibility lies in the scientific work itself, in the
  79. choices of presentation, and in the choice of Fossacs space limits
  80. which are exactly twice smaller than most other conferences in our
  81. domain.
  82.  
  83. We think of our work as presenting two distinct contributions:
  84.  
  85. - a conceptual contribution, drawing attention to the question of
  86. usable designs for multi-language programs (by discussing the
  87. context and examples), and proposing a *formal* specification for
  88. a class of "adding language L to the system does not break user
  89. expectations"
  90.  
  91. - a technical contribution, instantiating the conceptual proposal
  92. above by designing the language L, showing (through examples) that
  93. it is a useful side-kick to a typical ML-family programming language
  94. U, doing a metatheory of L and of UL together, and proving that they
  95. respect the formal specification (Full Abstraction).
  96.  
  97. The conceptual contribution takes only 2 pages, and we are reluctant
  98. to shorten it more: the contexts and explanation are the part of this
  99. work that could inspire others to reuse our proposed formal
  100. criterion -- our goal in publishing this work.
  101.  
  102. In the technical contribution, we have made the choice to delegate the
  103. technical proofs to the appendices, which Reviewer 1 apparently found
  104. problematic. We consider that the proof technique is not the main
  105. contribution of this work (it is not particularly technically
  106. challenging); we are happy to give access to a long preprint of this
  107. work with appendices (we already have a preprint on arXiv) for others
  108. to check our formal developments and reuse them in necessary, but we
  109. had decided to rather devote our exposition space to informal
  110. explanations of the language design of L, and the way UL is
  111. constructed from U and L (Reviewer 1 found this Section 3 confusing,
  112. possibly out of terseness).
  113.  
  114. Review 2 asks what a final version of this work, without Appendices,
  115. would look like. Our base plan was to have something like the current
  116. submission, with Appendices omitted (and without references to them in
  117. the main document). We warmly welcome any suggestion on main-body
  118. content that could be moved out, or appendix-content that we should
  119. really try to include.
  120.  
  121. Let us just review quickly the choices that were made for appendix
  122. content in the submission (feel free to skip that part):
  123.  
  124. A. Quicksort, which takes a lot of space and has the "red wall"
  125. effect. We don't think this is essential content -- it was there to
  126. demonstrate use-cases of L, but we can rely on our reader's
  127. imagination instead.
  128.  
  129. B. Internal syntax and typing. While this section is of interest to
  130. people designing languages with linear types, we think that users
  131. of the language or readers of the paper can skip it, as it can be
  132. summarized by "It is possible to show subject reduction for L."
  133.  
  134. C. Reduction of Internal Terms. (With apologies for the macro mistake
  135. in the submission...). The most interesting part of this section
  136. are the reduction rules for linear memory operations (new/free,
  137. box/unbox), and the operational semantics of "copy". We will
  138. consider adding them to the main manuscript.
  139.  
  140. D, E: static and dynamic semantics of UL. We could include an excerpt
  141. the type correspondence rules in the main manuscript (for example
  142. lump, product, function and bang), and the corresponding value
  143. correspondence rules (the function rules, which have to perform an
  144. eta-expansion, are interesting).
  145.  
  146. F. The full abstraction proof. We are of the opinion that the proof
  147. itself needs not be include in the short conference presentation of
  148. this work (it is not as interesting or original than the rest of
  149. the work), but welcome further feedback from the reviewers.
  150.  
  151. G and I. Parametricity, and the logical relation. The parametricity
  152. relation was built to substantiate, formally, the informal claim
  153. that the interaction between explicit lump types and type variables
  154. was a design improvement over previous multi-language designs
  155. (Perconti and Ahmed, 2014). This is an interesting result that
  156. required some amount of proving work but, in view of the space
  157. restrictions, we would not include it in the main article -- this
  158. is an unfortunate but classic case of removing scientific content
  159. to fit presentation constraints.
  160.  
  161. H. Hybrid program examples. We have no space in the main article for
  162. further examples, and we hope that the hope remains readable
  163. without them.
  164.  
  165.  
  166. # Other questions
  167.  
  168. ## Review 1
  169.  
  170. > - Section 3.3. What is the intuition behind Definition 1 and
  171. > Definition 2?
  172.  
  173. Contextual equivalence is a standard way to define a notion of
  174. equivalence of open term (with free/unbound variables) from a notion
  175. of equivalence on closed term at "ground" types in which equivalence
  176. is easy to define.
  177. (Typically, for a total language with only strongly terminating
  178. program, equivalence at closed program of boolean type is easy to
  179. define (they both return (true) or both return (false)). For
  180. a non-terminating language, termination properties must also be
  181. considered. For a language with input/output, the trace of
  182. user-observable actions during program execution must also be
  183. considered. These also correspond to natural choices of denotational
  184. semantics for these languages.)
  185.  
  186. Consider a fixed language and an equivalence relation
  187.  
  188. \emptyset |- t \simeq t' : tau
  189.  
  190. where (tau) belong to a class of "ground" types for which equivalence is
  191. easy to define. Then contextual equivalence of two open terms
  192.  
  193. (Gamma |- e : sigma) and (Gamma |- e' : sigma)
  194.  
  195. is defined by:
  196.  
  197. for any context (C) such as (C[e], C[e']) are closed terms at
  198. a ground type (tau), we have the closed program equivalence
  199. (\emptyset |- C[e] \simeq C[e'] : tau)
  200.  
  201. In definition 1, the "language" considered is just U, and the
  202. equivalence on closed terms is: two terms at unit type are equivalent
  203. if they are equi-terminating.
  204. This closed-program equivalence is a standard choice, which is
  205. equivalent to taking, for example, the boolean type as ground, and
  206. asking that the two programs either both diverge or return the same
  207. boolean value -- consider the contexts
  208. (if {hole} then () else {infinite loop}) and
  209. (if {hole} then {infinite loop} else ()).
  210.  
  211. In definition 2, the "language" considered is UL, and the notion of
  212. closed program equivalence is similar. For UL, we could consider
  213. comparing either two blue terms or two red terms (all terms have
  214. alternating layers of blue and red, but they either start with blue
  215. constructs or with red constructs), and having contexts that return
  216. either blue ground types or red ground types. But for the purpose of
  217. stating the full abstraction result, only the equivalence of blue
  218. terms matters.
  219.  
  220. > - Section 3.3. In the sequents of Theorem 2 you use a notation that
  221. > has not been defined (the equivalence of e and e' typed by \sigma)
  222.  
  223. Theorem 2 states that if two open U programs (e, e') are equivalent in
  224. the sense of Definition 1, then they are also equivalent in the sense
  225. of Definition 2.
  226.  
  227. ## Review 2
  228.  
  229. > Fig. 10 I am missing somewhere an stated invariant like
  230. >
  231. > if e : σ then ⟦e⟧ : ⟦σ⟧
  232. >
  233. > which I suppose is intended.
  234.  
  235. Yes, and also for contexts -- the type of the hole also gets
  236. translated in the expected way. Thanks for pointing this out (and for
  237. the many other careful, very helpful comments).
Add Comment
Please, Sign In to add comment