Campus Event Calendar
Event Entry
What and Who
Linear Higher-Order Pre-Unification
Frank Pfenning
CMU, z.Zt. TH Darmstadt
Logik-Seminar
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 5 July 96
14:15
60 Minutes
46.1 - MPII
019
Saarbrücken
Abstract
We describe a conservative extension of the simply-typed lambda-
calculus by -o (linear implication), & (additive conjunction)
and T (additive truth). The resulting calculus is the largest
conservative linear extension of the simply-typed lambda-calculus
permitting unique long beta-eta-normal forms. This property is
critical for the application of the calculus in a linear logical
framework (LLF) and its operational interpretation as a logic
programming language.
calculus by -o (linear implication), & (additive conjunction)
and T (additive truth). The resulting calculus is the largest
conservative linear extension of the simply-typed lambda-calculus
permitting unique long beta-eta-normal forms. This property is
critical for the application of the calculus in a linear logical
framework (LLF) and its operational interpretation as a logic
programming language.
The problem of unification in this lambda-calculus is, of course,
undecidable, but a pre-unification algorithm in the style of
Huet exists. We describe this algorithm and show that, perhaps
somewhat surprisingly, a similar algorithm does not exist for the
multiplicative-exponential fragment.
Contact
--email hidden
passcode not visible
logged in users only