Compiling with continuations, correctly

In this paper we present a novel simulation relation for proving correctness of program transformations that combines syntactic simulations and logical relations. In particular, we establish a new kind of simulation diagram that uses a small-step or big-step semantics in the source language and an untyped, step-indexed logical relation in the target language. Our technique provides a practical solution for proving semantics preservation for transformations that do not preserve reductions in the source language. This is common when transformations generate new binder names, and hence α-conversion must be explicitly accounted for, or when transformations introduce administrative redexes. Our technique does not require reductions in the source language to correspond directly to reductions in the target language. Instead, we enforce a weaker notion of semantic preorder, which suffices to show that semantics are preserved for both whole-program and separate compilation. Because our logical relation is transitive, we can transition between intermediate program states in a small-step fashion and hence the shape of the proof resembles that of a simple small-step simulation. We use this technique to revisit the semantic correctness of a continuation-passing style (CPS) transformation and we demonstrate how it allows us to overcome well-known complications of this proof related to α-conversion and administrative reductions. In addition, by using a logical relation that is indexed by invariants that relate the resource consumption of two programs, we are able show that the transformation preserves diverging behaviors and that our CPS transformation asymptotically preserves the running time of the source program. Our results are formalized in the Coq proof assistant. Our continuation-passing style transformation is part of the CertiCoq compiler for Gallina, the specification language of Coq.

Linguistic Mistakes

Ever since the publication of Kripke’s Wittgenstein on Rules and Private Language, there’s been a raging debate in philosophy of language over whether meaning and thought are, in some sense, normative. Most participants in the normativity wars seem to agree that some uses of meaningful expressions are semantically correct while disagreeing over whether this entails anything normative. But what is it to say that a use of an expression is semantically correct? On the so-called orthodox construal, it is to say that it doesn’t result in a factual mistake, that is, in saying or thinking something false. On an alternative construal it is instead to say that it doesn’t result in a distinctively linguistic mistake, that is, in misusing the expression. It is natural to think that these two construals of semantic correctness are simply about different things and not necessarily in competition with each other. However, this is not the common view. Instead, several philosophers who subscribe to the orthodox construal have argued that the alternative construal of correctness as use in accordance with meaning doesn’t make any sense, partly because there are no clear cases of linguistic mistakes (Whiting in Inquiry, 59:219–238, 2016, Wikforss in Philos Stud 102:203–226, 2001). In this paper I develop and defend the idea that there’s a distinctively linguistic notion of correctness as use in accordance with meaning and argue that there are clear cases of linguistic mistakes.

Linguodidactic correctness as a principle of foreign language teaching

Necessity to proceed to teaching foreign languages on a scientific basis and not to separate the linguistic aspect from the pedagogical and psychological was emphasized by the linguists in the last century. H. E. Palmer theoretically developed this requirement by introducing the term "principles of linguistic pedagogy" into scientific usage.The article analyses a problem that has become especially actual in modern linguodidactics, namely: the need to justify and adhere to the position that the language is described not "in itself and for itself", but taking into consideration the fact that its description should meet the obligatory needs of teaching language as means of transmitting information.The pedagogical approach to language makes the linguists admit that the structure of the language differs from other structures. First, it is an active dynamic model ("meaning – text"); secondly, it has several levels, and the most profound is fundamental. The following is the level of intentions, which is indirectly correlated with the level of meanings of words. Third, the action of the model is related to the direction of speech communication and the correctness of what is expressed in the speech utterance.An essential feature of modern pedagogical linguistics is to take into account the peculiarities of linguistic communication, which are manifested, in particular, in the correct usage of expressing means of the foreign language tools necessary for adequate exchange of ideas in the communication process.The article has clarified the following types of correctness: correctness usage of language behaviour, correct use of lexical units, correctness of syntactic forms, communicative correctness, semantic correctness, pragmatic correctness, and also defines the relationship between the concepts of correctness and speech etiquette.In general, the description of correctness in speech behaviour was performed within the framework of pedagogical tasks. For the first time, correctness has been studied as a deep principle of interaction of didactic laws with structural elements of language, which may have practical value for the development of innovative methods of teaching a foreign language.

How the Brain Understands Spoken and Sung Sentences

The present study investigates whether meaning is similarly extracted from spoken and sung sentences. For this purpose, subjects listened to semantically correct and incorrect sentences while performing a correctness judgement task. In order to examine underlying neural mechanisms, a multi-methodological approach was chosen combining two neuroscientific methods with behavioral data. In particular, fast dynamic changes reflected in the semantically associated N400 component of the electroencephalography (EEG) were simultaneously assessed with the topographically more fine-grained vascular signals acquired by the functional near-infrared spectroscopy (fNIRS). EEG results revealed a larger N400 for incorrect compared to correct sentences in both spoken and sung sentences. However, the N400 was delayed for sung sentences, potentially due to the longer sentence duration. fNIRS results revealed larger activations for spoken compared to sung sentences irrespective of semantic correctness at predominantly left-hemispheric areas, potentially suggesting a greater familiarity with spoken material. Furthermore, the fNIRS revealed a widespread activation for correct compared to incorrect sentences irrespective of modality, potentially indicating a successful processing of sentence meaning. The combined results indicate similar semantic processing in speech and song.

Method of verification the correctness of the air object recognition process

The basis of the developed procedure for verification the correctness of the process of recognition of airborne objects is the method of standards. The role of the standards is fulfilled by the introduced correctness constraints. During the control, the syntactic and semantic correctness of the recognition process are verified. The method differs from the known ones in the following. When verification certain types of semantic inaccuracy of descriptions of classes of alphabets, the concept of medium risk is used. The essence of the developed method for verification the differences in the descriptions of alphabet classes is as follows. The medium risk values are calculated when each pair of alphabet classes is recognized and the implementation of the restrictions introduced is verified. Using the method allows at the stage of debugging formalized knowledge to identify inaccuracies associated with the indistinguishability of alphabet classes and use the numerical value of the medium risk to identify other types of semantic inaccuracies. The essence of the developed method for verification the structural redundancy of alphabet class descriptions is as follows. The medium risk values are calculated during class recognition using various "fragments" of its description. The restriction introduced makes it possible to reveal indistinguishable “fragments” of class descriptions. Removing redundant descriptions reduces the time it takes to find solutions for classes of objects. The developed method for identifying the characteristic redundancy of class descriptions is also based on the procedure of calculating the medium risk value, adopted as a characteristic of the a priori information content of the signs. The method allows at the stage of filling the knowledge base to automate the identification and elimination of non-informative features in class descriptions, reduces the labor required to verify redundancy. At the stage of directly solving the recognition problem, the method allows to reduce computational costs by ranking the used features by their a priori information content and the corresponding organization of the search process for the decision on recognition classes of air objects.

Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing

We present semantic correctness proofs of Automatic Differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Finally, we sketch how the analysis extends to other AD methods by considering a continuation-based method.