Type-omega DPLs

Type-omega DPLs (Denotational Proof Languages) are languages for proof presentation and search that offer strong soundness guarantees. LCF-type systems such as HOL offer similar guarantees, but their soundness relies heavily on static type systems. By contrast, DPLs ensure soundness dynamically, through their evaluation semantics; no type system is necessary. This is possible owing to a novel two-tier syntax that separates deductions from computations, and to the abstraction of assumption bases, which is factored into the semantics of the language and allows for sound evaluation. Every type-omega DPL properly contains a type-alpha DPL, which can be used to present proofs in a lucid and detailed form, exclusively in terms of primitive inference rules. Derived inference rules are expressed as user-defined methods, which are "proof recipes" that take arguments and dynamically perform appropriate deductions. Methods arise naturally via parametric abstraction over type-alpha proofs. In that light, the evaluation of a method call can be viewed as a computation that carries out a type-alpha deduction. The type-alpha proof "unwound" by such a method call is called the "certificate" of the call. Certificates can be checked by exceptionally simple type-alpha interpreters, and thus they are useful whenever we wish to minimize our trusted base. Methods are statically closed over lexical environments, but dynamically scoped over assumption bases. They can take other methods as arguments, they can iterate, and they can branch conditionally. These capabilities, in tandem with the bifurcated syntax of type-omega DPLs and their dynamic assumption-base semantics, allow the user to define methods in a style that is disciplined enough to ensure soundness yet fluid enough to permit succinct and perspicuous expression of arbitrarily sophisticated derived inference rules. We demonstrate every major feature of type-omega DPLs by defining and studying NDL-omega, a higher-order, lexically scoped, call-by-value type-omega DPL for classical zero-order natural deduction---a simple choice that allows us to focus on type-omega syntax and semantics rather than on the subtleties of the underlying logic. We start by illustrating how type-alpha DPLs naturally lead to type-omega DPLs by way of abstraction; present the formal syntax and semantics of NDL-omega; prove several results about it, including soundness; give numerous examples of methods; point out connections to the lambda-phi calculus, a very general framework for type-omega DPLs; introduce a notion of computational and deductive cost; define several instrumented interpreters for computing such costs and for generating certificates; explore the use of type-omega DPLs as general programming languages; show that DPLs do not have to be type-less by formulating a static Hindley-Milner polymorphic type system for NDL-omega; discuss some idiosyncrasies of type-omega DPLs such as the potential divergence of proof checking; and compare type-omega DPLs to other approaches to proof presentation and discovery. Finally, a complete implementation of NDL-omega in SML-NJ is given for users who want to run the examples and experiment with the language.

Foundations of Actor Semantics

The actor message-passing model of concurrent computation has inspired new ideas in the areas of knowledge-based systems, programming languages and their semantics, and computer systems architecture. The model itself grew out of computer languages such as Planner, Smalltalk, and Simula, and out of the use of continuations to interpret imperative constructs within A-calculus. The mathematical content of the model has been developed by Carl Hewitt, Irene Greif, Henry Baker, and Giuseppe Attardi. This thesis extends and unifies their work through the following observations. The ordering laws postulated by Hewitt and Baker can be proved using a notion of global time. The most general ordering laws are in fact equivalent to an axiom of realizability in global time. Independence results suggest that some notion of global time is essential to any model of concurrent computation. Since nondeterministic concurrency is more fundamental than deterministic sequential computation, there may be no need to take fixed points in the underlying domain of a power domain. Power domains built from incomplete domains can solve the problem of providing a fixed point semantics for a class of nondeterministic programming languages in which a fair merge can be written. The event diagrams of Greif's behavioral semantics, augmented by Baker's pending events, form an incomplete domain. Its power domain is the semantic domain in which programs written in actor-based languages are assigned meanings. This denotational semantics is compatible with behavioral semantics. The locality laws postulated by Hewitt and Baker may be proved for the semantics of an actor-based language. Altering the semantics slightly can falsify the locality laws. The locality laws thus constrain what counts as an actor semantics.

Semantics-Preserving Dimensionality Reduction: Rough and Fuzzy-Rough-Based Approaches

R. Jensen and Q. Shen. Semantics-Preserving Dimensionality Reduction: Rough and Fuzzy-Rough Based Approaches. IEEE Transactions on Knowledge and Data Engineering, 16(12): 1457-1471. 2004.

Frequency of word-use predicts rates of lexical evolution throughout Indo-European history

Mark Pagel, Quentin D. Atkinson & Andrew Meade (2007). Frequency of word-use predicts rates of lexical evolution throughout Indo-European history. Nature, 449,717-720. RAE2008

What children learn from adults’ utterances: an ephemeral lexical boost and persistent syntactic priming in adult–child dialogue

We show that children’s syntactic production is immediately affected by individual experiences of structures and verb–structure pairings within a dialogue, but that these effects have different timecourses. In a picture-matching game, three- to four-year-olds were more likely to describe a transitive action using a passive immediately after hearing the experimenter produce a passive than an active (abstract priming), and this tendency was stronger when the verb was repeated (lexical boost). The lexical boost disappeared after two intervening utterances, but the abstract priming effect persisted. This pattern did not differ significantly from control adults. Children also showed a cumulative priming effect. Our results suggest that whereas the same mechanism may underlie children’s immediate syntactic priming and long-term syntactic learning, different mechanisms underlie the lexical boost versus long-term learning of verb–structure links. They also suggest broad continuity of syntactic processing in production between this age group and adults.

Aspects of Semantics and Pragmatics of Dialogue. SemDial 2010, 14th Workshop on the Semantics and Pragmatics of Dialogue

The papers collected in this book cover a range of topics in semantics and pragmatics of dialogue. All these papers were presented at SemDial 2010, the 14th Workshop on the Semantics and Pragmatics of Dialogue. This 14th edition in the SemDial series, also known as PozDial, took place in Poznań (Poland) in June 2010, and was organized by the Chair of Logic and Cognitive Science (Institute of Psychology, Adam Mickiewicz University). From over 30 submissions overall, 14 were accepted as full papers for plenary presentation at the workshop, and all are included in this book. In addition, 10 were accepted as posters, and are included here as 2-4 page short papers. Finally, we also include abstracts from our keynote speakers. We hope that the ideas gathered in this book will be a valuable source of up-to-date achievements in the field, and will become a valuable inspiration for new ones. We would like to express our thanks to all those who submitted to and participated in SemDial 2010, especially the invited speakers: Dale Barr (University of Glasgow), Jonathan Ginzburg (King's College London), Jeroen Groenendijk (University of Amsterdam) and Henry Prakken (Utrecht University, The University of Groningen). Last but not least, we would like to thank everybody engaged in the workshop organization -- the chairs, the local organizing committee for their hard work in Poznań, and the programme committee members for their thorough and helpful reviews.

A Formal Semantics for Weak References

A weak reference is a reference to an object that is not followed by the pointer tracer when garbage collection is called. That is, a weak reference cannot prevent the object it references from being garbage collected. Weak references remain a troublesome programming feature largely because there is not an accepted, precise semantics that describes their behavior (in fact, we are not aware of any formalization of their semantics). The trouble is that weak references allow reachable objects to be garbage collected, therefore allowing garbage collection to influence the result of a program. Despite this difficulty, weak references continue to be used in practice for reasons related to efficient storage management, and are included in many popular programming languages (Standard ML, Haskell, OCaml, and Java). We give a formal semantics for a calculus called λweak that includes weak references and is derived from Morrisett, Felleisen, and Harper’s λgc. λgc formalizes the notion of garbage collection by means of a rewrite rule. Such a formalization is required to precisely characterize the semantics of weak references. However, the inclusion of a garbage-collection rewrite-rule in a language with weak references introduces non-deterministic evaluation, even if the parameter-passing mechanism is deterministic (call-by-value in our case). This raises the question of confluence for our rewrite system. We discuss natural restrictions under which our rewrite system is confluent, thus guaranteeing uniqueness of program result. We define conditions that allow other garbage collection algorithms to co-exist with our semantics of weak references. We also introduce a polymorphic type system to prove the absence of erroneous program behavior (i.e., the absence of “stuck evaluation”) and a corresponding type inference algorithm. We prove the type system sound and the inference algorithm sound and complete.

Development of hemispheric specialization for lexical pitch-accent in Japanese infants.

Infants' speech perception abilities change through the first year of life, from broad sensitivity to a wide range of speech contrasts to becoming more finely attuned to their native language. What remains unclear, however, is how this perceptual change relates to brain responses to native language contrasts in terms of the functional specialization of the left and right hemispheres. Here, to elucidate the developmental changes in functional lateralization accompanying this perceptual change, we conducted two experiments on Japanese infants using Japanese lexical pitch-accent, which changes word meanings with the pitch pattern within words. In the first behavioral experiment, using visual habituation, we confirmed that infants at both 4 and 10 months have sensitivities to the lexical pitch-accent pattern change embedded in disyllabic words. In the second experiment, near-infrared spectroscopy was used to measure cortical hemodynamic responses in the left and right hemispheres to the same lexical pitch-accent pattern changes and their pure tone counterparts. We found that brain responses to the pitch change within words differed between 4- and 10-month-old infants in terms of functional lateralization: Left hemisphere dominance for the perception of the pitch change embedded in words was seen only in the 10-month-olds. These results suggest that the perceptual change in Japanese lexical pitch-accent may be related to a shift in functional lateralization from bilateral to left hemisphere dominance.

La Web Semántica y los archivos de televisión: estado de la cuestión

Se analizan y describen las principales líneas de trabajo de la Web Semántica en el ámbito de los archivos de televisión. Para ello, se analiza y contextualiza la web semántica desde una perspectiva general para posteriormente analizar las principales iniciativas que trabajan con lo audiovisual: Proyecto MuNCH, Proyecto S5T, Semantic Television y VideoActive.

P300 investigation of phoneme change detection in dyslexic adults

A specific impairment in phoneme awareness has been hypothesized as one of the current explanations for dyslexia. We examined attentional shifts towards phonological information as indexed by event-related potentials (ERPs) in normal readers and dyslexic adults. Participants performed a lexical decision task on spoken stimuli of which 80% started with a standard phoneme and 20% with a deviant phoneme. A P300 modulation was expected for deviants in control adults, indicating that the phonological change had been detected. A mild and right-lateralized P300 was observed for deviant stimuli in controls, but was absent in dyslexic adults. This result suggests that dyslexic adults fail to make shifts of attention to phonological cues in the same way that normal adult readers do. (C) 2003 Elsevier Ireland Ltd. All rights reserved.

Phonological oddballs in the focus of attention elicit a normal P3b in dyslexic adults

Difficulties in phonological processing have been proposed to be the core symptom of developmental dyslexia. Phoneme awareness tasks have been shown to both index and predict individual reading ability. In a previous experiment, we observed that dyslexic adults fail to display a P3a modulation for phonological deviants within an alliterated word stream when concentrating primarily on a lexical decision task [Fosker and Thierry, 2004, Neurosci. Lett. 357, 171-174]. Here we recorded the P3b oddball response elicited by initial phonemes within streams of alliterated words and pseudo-words when participants focussed directly on detecting the oddball phonemes. Despite significant verbal screening test differences between dyslexic adults and controls, the error rates, reactions times, and main components (P2, N2, P3a, and P3b) were indistinguishable across groups. The only difference between groups was found in the NI range, where dyslexic participants failed to show the modulations induced by phonological pairings (/b/-/p/ versus /r/ /g/) in controls. In light of previous P3a differences, these results suggest an important role for attention allocation in the manifestation of phonological deficits in developmental dyslexia. (c) 2005 Elsevier B.V. All rights reserved.

Annotating an Oral Corpus using the Text Encoding Initiative. Methodology, Problems, Solutions

The objective of this paper is to describe and evaluate the application of the Text Encoding Initiative (TEI) Guidelines to a corpus of oral French, this being the first corpus of oral French where the TEI has been used. The paper explains the purpose of the corpus, both in creating a specialist corpus of néo-contage that will broaden the range of oral corpora available, and, more importantly, in creating a dataset to explore a variety of oral French that has a particularly interesting status in terms of factors such as conception orale/écrite, réalisation médiale and comportement communicatif (Koch and Oesterreicher 2001). The linguistic phenomena to be encoded are both stylistic (speech and thought presentation) and syntactic (negation, detachment, inversion), and all represent areas where previous research has highlighted the significance of factors such as medium, register and discourse type, as well as a host of linguistic factors (syntactic, phonetic, lexical). After a discussion of how a tagset can be designed and applied within the TEI to encode speech and thought presentation, negation, detachment and inversion, the final section of the paper evaluates the benefits and possible drawbacks of the methodology offered by the TEI when applied to a syntactic and stylistic markup of an oral corpus.