Structural operational semantic specifications come in different styles: small-step and big-step. A problem with the big-step style is that specifying divergence and abrupt termination gives rise to annoying duplication. We present a novel approach to representing divergence and abrupt termination in big-step semantics using status flags. This avoids the duplication problem, and uses fewer rules and premises for representing divergence than previous approaches in the literature.
Several papers have explored how to represent divergence in big-step semantics. Leroy and Grall @cite_0 survey different approaches to representing divergence in coinductive big-step semantics, including divergence predicates, trace-based semantics, and taking the coinductive interpretation of standard big-step rules. They conclude that traditional divergence predicates are the most well-behaved, but increase the size of specifications by around 40 infinite traces for accumulating the full trace of rules with multiple premises. Nakata and Uustalu @cite_35 propose a more elegant approach to accumulating traces based on peel' rules. Their approach is closely related to the , introduced by Capretta, and used by several authors to give functional representations of big-step semantics, including Danielsson @cite_10 and Abel and Chapman @cite_21 (who call it the ). In the partiality monad, functions either return a finitely delayed result or an infinite trace of delays. Pir ' o g and Gibbons @cite_39 study the category theoretic foundations of the resumption monad. Related to the resumption monad is the interactive I O monad by Hancock and Setzer @cite_12 for modeling the behaviour of possibly-diverging interactive programs.
@cite_35 @cite_21 @cite_39 @cite_0 @cite_10 @cite_12
1990062016 1982866418 2169488840 2949804971
We look at the operational semantics of languages with interactive I O through the glasses of constructive type theory. Following on from our earlier work on coinductive trace-based semantics for While [17], we define several big-step semantics for Whil e with interactive I O, based on resumptions and termination-sensitive weak bisimilarity. These require nesting inductive definitions in coinductive definitions, which is interesting both mathe matically and from the point-of-view of implementation in a proof assistant. After first defining a basic semantics of statements in terms o f resumptions with explicit internal actions (delays), we introduce a semantics in terms of delay-free resumptions that essentially removes finite sequences of delays on the fly from those resumptions th at are responsive. Finally, we also look at a semantics in terms of delay-free resumptions supplemented with a silent divergence option. This semantics hinges on decisions between convergence and divergence and is only equivalent to the basic one classically. We have fully formalized our development in Coq. Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results. Big-step semantics for languages with abrupt termination and or divergence suffer from a serious duplication problem, addressed by the novel 'pretty-big-step' style presented by Chargueraud at ESOP'13. Such rules are less concise than corresponding small-step rules, but they have the same advantages as big-step rules for program correctness proofs. Here, we show how to automatically derive pretty-big-step rules directly from small-step rules by 'refocusing'. This gives the best of both worlds: we only need to write the relatively concise small-step specifications, but our reasoning can be big-step as well as small-step. The use of strictness annotations to derive small-step congruence rules gives further conciseness. We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integrating over all traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language.