Refine
Document Type
- Part of a Book (23)
- Working Paper (14)
- Article (2)
- Doctoral Thesis (2)
Language
- English (41)
Has Fulltext
- yes (41)
Is part of the Bibliography
- no (41)
Keywords
- Formale Semantik (41) (remove)
Institute
- Informatik (11)
- Neuere Philologien (1)
This article develops a Gricean account for the computation of scalar implicatures in cases where one scalar term is in the scope of another. It shows that a cross-product of two quantitative scales yields the appropriate scale for many such cases. One exception is cases involving disjunction. For these, I propose an analysis that makes use of a novel, partially ordered quantitative scale for disjunction and capitalizes on the idea that implicatures may have different epistemic status.
The interpretation of traces
(2004)
This paper argues that parts of the lexical content of an A-bar moved phrase must be interpreted in the base position of movement. The argument is based on a study of deletion of a phrase that contains the base position of movement. I show that deletion licensing is sensitive to the content of the moved phrase. In this way, I corroborate and extend conclusions based on Condition C reconstruction by N. Chomsky and D. Fox. My result provides semantic evidence for the existence of traces and gives semantic content to the A/A-bar distinction.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. It is designed to perform automatic induction proofs and can also deal with partial functions. This paper provides a reconstruction of the corresponding logic and semantics using the standard treatment of undefinedness which adapts and improves the VeriFun-logic by allowing reasoning on nonterminating expressions and functions. Equality of expressions is defined as contextual equivalence based on observing termination in all closing contexts. The reconstruction shows that several restrictions of the VeriFun framework can easily be removed, by natural generalizations: mutual recursive functions, abstractions in the data values, and formulas with arbitrary quantifier prefix can be formulated. The main results of this paper are: an extended set of deduction rules usable in VeriFun under the adapted semantics is proved to be correct, i.e. they respect the observational equivalence in all extensions of a program. We also show that certain classes of theorems are conservative under extensions, like universally quantified equations. Also other special classes of theorems are analyzed for conservativity.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. This paper provides a reconstruction of the corresponding logic when partial functions are permitted. Typing is polymorphic for the definition of functions but monomorphic for terms in formulas. Equality of terms is defined as contextual equivalence based on observing termination in all contexts. The reconstruction also allows several generalizations of the functional language like mutual recursive functions and abstractions in the data values. The main results are: Correctness of several program transformations for all extensions of a program, which have a potential usage in a deduction system. We also proved that universally quantified equations are conservative, i.e. if a universally quantified equation is valid w.r.t. a program P, then it remains valid if the program is extended by new functions and/or new data types.
The calculus CHF models Concurrent Haskell extended by concurrent, implicit futures. It is a process calculus with concurrent threads, monadic concurrent evaluation, and includes a pure functional lambda-calculus which comprises data constructors, case-expressions, letrec-expressions, and Haskell’s seq. Futures can be implemented in Concurrent Haskell using the primitive unsafeInterleaveIO, which is available in most implementations of Haskell. Our main result is conservativity of CHF, that is, all equivalences of pure functional expressions are also valid in CHF. This implies that compiler optimizations and transformations from pure Haskell remain valid in Concurrent Haskell even if it is extended by futures. We also show that this is no longer valid if Concurrent Haskell is extended by the arbitrary use of unsafeInterleaveIO.
Russian predicate cleft constructions have the surprising property of being associated with adversative clauses of the opposite polarity. I argue that clefts are associated with adversative clauses because they have the semantics of S-Topics in Büring's (1997, 2000) sense of the term. It is shown that the polarity of the adversative clause is obligatorily opposed to that of the cleft because the use of a cleft gives rise to a relevance-based pragmatic scale. The ordering principle according to which these scale