Refine
Year of publication
- 2010 (84) (remove)
Document Type
- Working Paper (84) (remove)
Has Fulltext
- yes (84)
Is part of the Bibliography
- no (84) (remove)
Keywords
- Film (4)
- Formale Semantik (4)
- Argumentationstheorie (3)
- Finanzkrise (3)
- Internetsprache (3)
- Logik (3)
- Normative Ordnungen (3)
- Verifikation (3)
- Asset Allocation (2)
- Außenpolitik (2)
Institute
- Center for Financial Studies (CFS) (29)
- Exzellenzcluster Die Herausbildung normativer Ordnungen (12)
- Institute for Law and Finance (ILF) (11)
- Informatik (6)
- Institute for Monetary and Financial Stability (IMFS) (6)
- Extern (4)
- Wirtschaftswissenschaften (4)
- Gesellschaftswissenschaften (3)
- Institut für sozial-ökologische Forschung (ISOE) (2)
- Medizin (2)
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 well-known proof of termination of reduction in simply typed calculi is adapted to a monomorphically typed lambda-calculus with case and constructors and recursive data types. The proof differs at several places from the standard proof. Perhaps it is useful and can be extended also to more complex calculi.
Dieses Arbeitspapier geht aus einem Hauptseminar zur Argumentationstheorie hervor, das [von Leila Behrens] im Wintersemester 2008/09 am Institut für Linguistik der Universität zu Köln gehalten [wurde]. In den beiden Arbeiten in diesem Band (Badtke et al. und Benning et al.) stellen die Studierenden dieses Hauptseminars die Ergebnisse vor, die sie (in zwei parallelen Projektgruppen mit unterschiedlichen Diskussionsgegenständen) bei der empirischen Analyse von Argumentationen in einem Internet-Forum gewonnen haben. Der Gegenstand der Diskussion betraf bei der einen Gruppe (Badtke et al.) die Unabhängigkeit des Kosovo, bei der anderen Gruppe (Benning et al.) die Einführung eines generellen Rauchverbots in europäischen Hauptstädten.