FREE ELECTRONIC LIBRARY - Abstract, dissertation, book

Pages:   || 2 | 3 | 4 |

«Edited by Maribel Fern´ndez a Chris Fox Shalom Lappin King’s College London Strand, London, U.K. 8th –9th December 2003 Workshop on Lambda ...»

-- [ Page 1 ] --

Lambda Calculus

Type Theory


Natural Language

Edited by

Maribel Fern´ndez


Chris Fox

Shalom Lappin

King’s College London

Strand, London, U.K.

8th –9th December 2003

Workshop on Lambda Calculus, Type Theory, and Natural Language

King’s College London, Strand, London, U.K., 8th–9th December 2003


Maribel Fern´ndez

a maribel@dcs.kcl.ac.uk

Chris Fox foxcj@essex.ac.uk

Shalom Lappin lappin@dcs.kcl.ac.uk


David Clark King’s College London, U.K.

Robin Cooper G¨teborg University, Sweden o Maribel Fern´ndez a King’s College London, U.K.

Chris Fox University of Essex, U.K.

Dov Gabbay King’s College London, U.K.

Jamie Gabbay INRIA Futurs, France Simon Gay University of Glasgow, U.K.

Jonathan Ginzburg King’s College London, U.K.

Chris Hankin Imperial College, U.K.

Shalom Lappin King’s College London, U.K.

Ian Mackie King’s College London, U.K.

Francois-Regis Sinot Ecole Polytechnique, France Ray Turner University of Essex, U.K.

Key Note Speaker:

Jan van Eijck CWI, Netherlands


Department of Computer Science Department of Computer Science King’s College London University of Essex Strand Wivenhoe Park London WC2R 2LS Colchester CO4 3SQ United Kingdom United Kingdom http://www.dcs.kcl.ac.uk http://cswww.essex.ac.uk Programme Monday, 8th December.

9:30 Coffee — Welcome 10:00 Opening 10:15 Chris Hankin.

Lambda calculus and static analysis.

11:00 Coffee Break 11:30 Ian Mackie.

Reduction in the lambda calculus.

12:15 Francois-Regis Sinot.

N-ary director strings: Efficient representations of variables in terms.

13:00 Lunch 14:00 Jan van Eijck.

Relations, Types and Scoping.

15:00 Chris Fox and Shalom Lappin.

Underspecified Representations for Natural Language using Curry-typed λCalculus.

15:45 Coffee Break 16:15 Robin Cooper.

Records and record types in semantic theory.

17:00 Jonathan Ginzburg.

Abstraction and Ontology.

19:00 Dinner Tuesday, 9th December.

9:30 Coffee 10:00 Maribel Fernandez.

Rewriting Frameworks and Types.

10:45 David Clark.

Measuring interference in PCF.

11:30 Coffee Break 12:00 Jamie Gabbay and Dov Gabbay.

The restart rule and evaluation.

12:45 Lunch 14:00 Ray Turner.

Polymorphism in Specifications.

14:45 Simon Gay.

Session Types: Specifying Structured Communication.

15:30 Closing

–  –  –

The Workshop on Lambda Calculus, Type Theory, and Natural Language (LCTTNL) is designed to bring together researchers interested in functional programming, type theory, and the application of the lambda calculus to the analysis of natural language. The communities that have developed around each of these areas share many formal and computational interestes. Unfortunately, they have not had much contact with each other. We hope that LCTTNL will provide a forum in which people working on the lambda calculus from a variety of distinct perspectives will share their research and come to appreciate new domains of application. If this encounter is successful, it can provide the basis for future cooperation and ongoing meetings of this kind.

We would like to thank the Computer Science Departments of King’s College London and the University of Essex for sponsorship and financial support. We are grateful to the speakers for their participation, and to our keynote speaker, Jan van Eijck, for agreeing to present his lecture.

–  –  –

Many arguments for flexible type assignment to syntactic categories have to do with the need to account for the various scopings resulting from the interaction of quantified DPs with other quantified DPs or with intensional or negated verb contexts.

We will define a type for arbitrary arity relations in polymorphic type theory. In terms of this, we develop the Boolean algebra of relations as far as needed for natural language semantics. The type for relations is flexible: it can do duty for the whole family of types t, e → t, e → e → t, and so on.

If we use this flexible type for the interpretations of verbs, we can perform a ‘flexible lift’ on DP interpretations, so that DPs get interpreted as operations on verb meanings. This leads to an elegant implementation of Keenan’s proposal for polyadic quantification in natural language (‘Beyond the Frege Boundary’). It turns out that scope reorderings are particularly easy to implement in this framework.

Measuring Interference in PCF (abstract) D. Clark, S. Hunt and P. Malacaria In recent work we have developed a security analysis for a simple imperative (while) language which has measured the leakage of secrets from confidential variables to a low security attacker via observation of the low security outputs from the execution of a program [1]. The analysis uses information theory to quantify the leakage and takes an information theoretic view: the quantity of information supplied to the program is taken to be the upper limit on the amount of information induced by the probability distribution on inputs (or entropy) as given by Shannon [4]. This analysis is based not on the syntax of the program per se but on a use definition graph (UDG) which is derived from the flow chart of the program and relates each use of a variable in an expression to its previous definition. The analysis uses this graph to trace the flow of information through the program. In the course of the analysis it is necessary to associate random variables with program variables and expressions. The analysis proceeds as a forward analysis, propagating bounds on the entropic measure of confidential information associated with the value at a program point of each variable or expression.

We have speculated that this approach could be applied to a functional language not too distant from the typed lambda calculus but containing delta rules for arithmetic, such as an enriched PCF. This would rely on using a version of the control flow analysis (CFA) based on game semantics for PCF as developed by Malacaria and Hankin [3]. To date we have yet to define a suitable notion of random variable for this CFA. This difficulty has caused us to examine anew the relationship between program variables, program points, and random variables [2] out of which has come the basis for this talk.

In this talk we examine another possible approach to quantifying interference between variables in a PCF program. The approach is quite general and could possibly be applied to any program whose semantics can be given as a function. We establish a relationship between program variables, random variables and equivalence relations and show how this relationship allows us to set an upper bound on the interference between variables at the beginning and the end of the program. We illustrate the power of the approach by means of examples. A feature of this approach is the separation between the qualitative and quantitative aspects of the analysis. The key notion is that constraints on the observation of outputs induce an equivalence relation on inputs (which may be interpreted as a random variable). This equivalence relation is the “coarsest” which is consistent with the constraints given the semantics of the program. An upper bound on the entropy of the random variable may be found by discovering any “finer” equivalence class on inputs. A way of doing this consistent with the program semantics is via an



References [1] D. Clark, S. Hunt, and P. Malacaria. Quantified interference for a while language. submitted to ESOP’04.

[2] D. Clark, S. Hunt, and P. Malacaria. Quantified interference: information theory and information flow security. submitted to QAPL’04.

[3] P. Malacaria and C. Hankin. A new approach to control flow analysis. In Poceedings of CC’98, 1998.

[4] Claude Shannon. A mathematical theory of communication. The Bell System Technical Journal, 27:379–423 and 623–656, July and October 1948. Available on-line at http://cm.bell-labs.com/cm/ms/what/shannonday/paper.html.

Rewriting Frameworks and Types Maribel Fern´ndez a King’s College London Rewriting systems are usually defined by specifying a set of terms, and a set of rewrite rules that are used to “reduce” terms. This simple idea is very powerful, and has had deep influence in the development of computational models, programming and specification languages, theorem provers and proof assistants. Term rewriting systems can be used to define,

amongst others:

• first-order equational theories: terms are built out of first-order functions and variables and rewrite rules define an equality relation. We obtain in this case the standard (firstorder) term rewriting systems, sometimes called algebraic systems.

• a theory of functions: Church’s λ-calculus was designed as a notation for functions,

using λ-abstraction, application and variables. The main rewrite rule is β-reduction:

–  –  –

The right hand side of this rule includes a substitution, which is not part of the syntax of λ-terms: it is a meta-operation defined modulo α-conversion since λ is a binder. This is an example of “higher-order” rule.

• higher-order equational theories, using first- and higher-order functions and variables:

we obtain in this case higher-order algebraic systems.

• a generalization of the previous cases, where terms are defined using functions, variables and binders. These are usually called higher-order rewriting systems, and can be divided

in two classes:

Algebraic λ-calculi: the syntax of the λ-calculus is enriched with algebraic functions, and the β-reduction rule is combined with algebraic rewrite rules. This kind of rewrite system is used as a computational model for functional programming languages and proof assistants.

First-order rewriting extended with a general notion of binder: Examples of systems in this class are Klop’s Combinatory Reduction Systems (CRS), Khasidashvili’s Expression Reduction Systems, Nipkow’s Higher-Order Rewrite Systems, and the ρ-calculus of Cirstea and Kirchner.

From the computational point of view all the systems mentioned above are equally powerful (they are all Turing complete), but from the point of view of their expressive power there are clear differences. The systems in the last class are the most expressive. For instance, it is easy to specify the λ-calculus, object-calculi (e.g. Abadi and Cardelli’s ς-calculus), and process calculi (e.g. the π-calculus), using Combinatory Reduction Systems (see [7]).

Although rewriting can be defined on untyped terms, for most of the formalisms mentioned above some notion of typing has been defined. Types can be used to define semantic interpretations for terms and rewrite rules, as specifications of programs defined by rewrite rules, as a link between computation and logic (as in the typed versions of the λ-calculus), etc. When combining λ-calculus with algebraic rewriting, type disciplines provide an environment in which rewrite rules and β-reduction can interact without loss of their useful properties [4, 6, 3].

Type disciplines come in two main flavours: explicitly typed systems (` la Church), and a type inference systems (` la Curry) which do not require type annotations. An important a feature of type systems is a notion of principal type, that is, a type from which all the other types of a term can be derived, or more generally, a notion of principal typing. The latter means that any typing judgement for a term can be obtained from the principal one, that is, not only the type but also the basis (containing the type assumptions for the free variables) is obtained. Unlike principal types, principal typings provide support for separate compilation, incremental type inference, and for accurate type error messages.

In the context of the λ-calculus type inference disciplines have been extensively studied, and type inference is now standard in functional languages (e.g. ML and Haskell). ML’s type system is polymorphic and has principal types, but does not have principal typings. System F provides a much more general notion of polymorphism, but lacks principal typings and type inference is undecidable in general (although it is decidable for some subsystems, in particular if we consider types of rank 2).The intersection type discipline [5] is an extension of Curry’s system that consists of allowing more than one type for variables and terms, considering the type constructor ∩ in addition to the arrow. Intersection type systems have principal typings (but are also undecidable above rank 2), and can be used to characterize normalization of λterms. Adding intersection types to System F, Margaria and Zacchi obtained a very powerful type system for the λ-calculus, which has principal typings.

Type inference for algebraic term rewriting systems or more general higher-order rewriting systems has attracted less attention. In some cases, it is possible to translate a term rewriting system into the λ-calculus and use the type systems mentioned above. However, this imposes strong restrictions in the rewrite rules. For example, adding the rewrite rules defining surjective pairing to the λ-calculus gives a system in which the Church-Rosser property no longer holds, which implies that surjective pairing is not definable in the λ-calculus.

Pages:   || 2 | 3 | 4 |

Similar works:

«Animate 2 User Guide Legal Notices Published by Toon Boom Animation Inc. Corporate Headquarters 5530 St. Patrick Suite2210 Montreal, Quebec Canada H4E 1A8 Tel: (514) 278-8666 Fax: (514) 278-2666 toonboom.com Disclaimer The content of this manual is covered by a specific limited warranty and exclusions and limit of liability under the applicable License Agreement as supplemented by the special terms and conditions for Adobe® Flash® File Format (SWF). Please refer to the License Agreement and...»

«Sport Nach Der Lebensmitte Not them have it to encourage the foreclosure property if this problems so that they face ideal. It can much drag the home in iPhones into an in-stock when they receive throwing and only you'm to have sole to drive to we. Hong APR did, Accolo real comparison feels your serving conversion. Also, possibility of one is the months of blows of best records. A affordable article for a compliance may long convince all the open anyone concept, to dispute online to as pick you...»

«Master of Theology in Practical Theology at Cardiff University (SHARE), St Michael’s College and the South Wales Baptist College 2012-13 A Cardiff University Degree, delivered in partnership with St Michael’s College and South Wales Baptist College. **** Possible Changes **** All students are hereby notified that the modules advertised or referred to in this handbook can be changed or withdrawn both before and after selection. Furthermore, the schedule of the modules may be liable to...»

«Finite-Time Singularity Signature of Hyperinflation arXiv:physics/0301007v1 [physics.soc-ph] 6 Jan 2003 D. Sornette a,b,c, H. Takayasu d, W.-X. Zhou a a Institute of Geophysics and Planetary Physics University of California, Los Angeles, CA 90095 b Department of Earth and Space Sciences University of California, Los Angeles, CA 90095 c Laboratoire de Physique de la Mati`re Condens´e, CNRS UMR 6622 and e e Universit´ de Nice-Sophia Antipolis, 06108 Nice Cedex 2, France e d SonyComputer...»

«Dissertation Submitted to the Combined Faculties for the Natural Sciences and for Mathematics of the Ruperto-Carola University of Heidelberg, Germany for the degree of Doctor of Natural Sciences Presented by Master of Science (M.Sc. Biotechnology) Kirti Shukla Born in: New Delhi, India Oral examination: 5.11.2014 Regulation of NF-κB signaling and cell cycle progression by microRNA-30c-2-3p in breast cancer Referees: Prof. Dr. Stefan Wiemann Prof. Dr. Petra Kioschis Thesis Declaration I hereby...»

«Religions 2015, 6, 891–911; doi:10.3390/rel6030891 OPEN ACCESS religions ISSN 2077-1444 www.mdpi.com/journal/religions Article Redefining Religious Nones: Lessons from Chinese and Japanese American Young Adults Russell Jeung1,*, Brett Esaki 2 and Alice Liu 3 Asian American Studies Department, San Francisco State University, 1600 Holloway Avenue EP103, San Francisco, CA 94132, USA Department of Religious Studies, Georgia State University, P.O. Box 3994, Atlanta, GA 30302-3994, USA; E-Mail:...»

«Marx, P. & Lenhard, W. (2010). Diagnostische Merkmale von Screeningverfahren. In M. Hasselhorn & W. Schneider (Hrsg), Frühprognose schulischer Kompetenzen. Göttingen: Hogrefe. Diagnostische Merkmale von Screening-Verfahren zur Früherkennung möglicher Probleme beim Schriftspracherwerb Peter Marx und Wolfgang Lenhard Zusammenfassung Möglichst frühzeitige Hinweise auf Beeinträchtigungen im Erwerb der grundlegenden schulischen Fertigkeiten Lesen und Rechtschreiben können zweifellos von...»

«Exhibit 1.01 Conflict Minerals Report Telefonaktiebolaget LM Ericsson Conflict Minerals Report for the year ended December 31, 2015 This Conflict Minerals Report of Telefonaktiebolaget LM Ericsson for the year ended December 31, 2015 is provided pursuant to Rule 13p-1 under the Securities Exchange Act of 1934, as amended (the “Rule”). The Rule was adopted by the U.S. Securities and Exchange Commission (the “SEC”) to implement disclosure and reporting requirements pursuant to Section...»

«The Civic Potential of Video Games This report was made possible by grants from the John D. and Catherine T. MacArthur Foundation in connection with its grant making initiative on Digital Media and Learning. For more information on the initiative visit www.macfound.org. The John D. and Catherine T. MacArthur Foundation Reports on Digital Media and Learning The Future of Learning Institutions in a Digital Age by Cathy N. Davidson and David Theo Goldberg with the assistance of Zoë Marie Jones...»

«Balogh Jolán Kolozsvári kőfaragó műhelyek XVI. század Testvérhugom, munkatársam Dr. Balogh Ilonka emlékezetére Balogh Jolán Kolozsvári kőfaragó műhelyek XVI. század Budapest, 1985 A Magyar Tudományos Akadémia Művészettörténeti Kutató Csoportjának kiadványa technikai szerkesztő: Beke László, Marosi Ernő helyés névmutató: Nováky Hajnalka címlapterv: Makky Mária A címlapon: Seres János sírköve. 1579. Részlet A belső címlapon: Seres János mesterjegye...»

«Reduced Model for Flow Simulation in the Burner Region of Lime Shaft Kilns Dissertation zur Erlangung des akademischen Grades Doktoringenieur (Dr.-Ing.) vorgelegt von M.Sc. Zhiguo Xu geb. am 04.02.1978 in Heze, Shandong, China genehmigt durch die Fakult¨t f¨r Verfahrensund Systemtechnik au der Otto-von-Guericke-Universit¨t Magdeburg a Gutachter: Prof. Dr.-Ing. E. Specht, Universit¨t Magdeburg a Prof. Dr.-Ing. D. Thevenin, Universit¨t Magdeburg a eingereicht am 01.03.2007...»

«List of all stolen works of art from the Ermitage, including already returned items This list has been edited and corrected by © Verlag Dr. Christian Müller-Straten, Munich 1. Crystal vase in the shape of a shell, on a crystal base, with carved ornamentation in a varicoloured enamel coated silver frame. The lower part of the stem is in the shape of a dolphin, and the handle is shaped like two snakes. 19th cent.2. Vase made from variegated brown agate, oval on a silver support that is covered...»

<<  HOME   |    CONTACTS
2016 www.abstract.xlibx.info - Free e-library - Abstract, dissertation, book

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.