Here, the availability of a single underlying proof system provides a new and unique opportunity to compare strategies on an equal footing. Measurement: The project will use normalization in deep inference to construct a range of semantic tools to measure the efficiency of these calculi and control mechanisms. These will be used to implement various efficient strategies with sharing and unsharing in typed lambda-calculi and abstract machines. Based on the experience with the atomic lambda-calculus, the hypothesis is that the proof system adapts naturally to different levels of efficiency by varying the choice of proof rules.Ĭontrol: New control mechanisms will be derived from the structure of deep inference proofs. Structure: The project will develop a theory of proof normalization in deep inference for intuitionistic logic (associated with the lambda-calculus), where the medial replaces the need for a control mechanism. The project will build on this on three levels: structure, control, and measurement.
#Typed lambda calculus full#
An initial investigation led to the atomic lambda-calculus, the first typed lambda-calculus with sharing and unsharing, and the first lambda-calculus to capture full laziness, a standard notion of efficiency, as a natural strategy. The project will develop a computational interpretation of the medial. The discovery on which the project is based is that the medial rule scheme enables computation with sharing and unsharing, as in sharing graphs, but without the need for a control mechanism other than the structure of the proof itself. However, in a real-world setting, the control mechanism that manages duplication, the oracle, incurs too much overhead cost, and they are not used in practice. In theory, sharing graphs are optimally efficient for lambda-calculus.
Unsharing is a counterpart that enables the shared use of partial expressions. Sharing is the multiple use of a single expression, which then needs to be evaluated only once, improving efficiency. Sharing graphs are a graphical formalism for lambda-calculus computation using sharing and unsharing. The basis of the project is the discovery that the medial enables computation steps associated with optimal efficiency. Key to these results is the medial rule scheme, a core innovation of deep inference that sets it apart from related formalisms. This allows it to capture logics not expressible in other proof systems, and to yield surprisingly good complexity results.
Conversely, for a given proof system we can ask what its computational interpretation is.ĭeep inference is a modern branch of proof theory characterized by its flexibility in composing proofs. The lambda-calculus is linked to proof theory by the Curry-Howard correspondence: types are logical formulas, programs are proofs, and computation is proof normalization (reduction to a well-behaved form).
Such improvements can be efficient computation strategies, or changes to the syntax, or both. It forms the basis of functional programming languages such as Haskell, and efficiency improvements in the lambda-calculus can be applied to create compilers that produce faster programs. The lambda-calculus is a minimal but fully expressive, theoretical programming language. This project aims to develop a new approach to efficient evaluation in the lambda-calculus, based on deep-inference proof theory.
0 kommentar(er)
