Inadvertently typed λ-join-calculus
Coq Python Other
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
doc
sandbox
src
.gitignore
.travis.yml
LICENSE
Makefile
README.md
install_coq.sh
metrics.py
requirements.txt

README.md

Build Status Proof Status

Holes File
10 BohmTrees
10 Types
8 LeastFixedPoint
7 TypeConstructor
6 Compile
6 StrongConstructor
5 Annotate
4 Codes
4 DeBruijn
3 Combinators
3 InformationOrdering
2 Nontermination

Inadvertently typed λ-join-calculus

This project aims to provide a Coq library to formally reason about two untyped λ-calculi that act like typed λ-calculi.

Introduction

In the early 1970's Dana Scott [1] developed an idiom of implementing data types as nondecreasing idempotent functions in lattice models of untyped λ-calculus. Scott's original work showed that this types-as-closures idiom leads to a rich type structure in D and P(ω) models, although the type system is inconsistent under the Curry-Howard correspondence due to the presence of a top element that inhabits every type. More recently, [2] showed that many of the atomic datatypes are definable with only λ-calculus and a binary join operator, after a suitable extensional collapse by Hyland and Wadsworth's axiom H*:

M = N   iff   forall context C[ ], C[M] converges <-> C[N] converges

The Coq developments in this project attempt to formalize the construction in [2] and extend the result to probabilistic programming languages, similar to Jean Goubault-Larrecq's recent full-abstraction result [3]. We reason in a language of ordered combinatory algebras, treating the Scott ordering [= as the basic relation. We develop type systems within two untyped universes and obtain algebraic types such as a -> b := \f. b o f o a. The type system supports algebraic, dependent, polymorphic, and intersection types, as well as atomic types and a type of all types; for example

I [= a    a = a o a            a : type    a x = x
=================== closures   =================== fixedpoints
      a : type                        x : a

forall x:a, f x [= g x
======================== universal quantification
          f o a [= g o a

a : type    b : type    a : type    b : type    a : type    b : type
--------------------    --------------------    --------------------
   a -> b : type            a * b : type            a + b : type

---------    -----------    ----------
TOP : typ    bool : type    nat : type

The main goal is to prove a set of induction principles supporting case analysis for well typed terms, for example:

                          p TOP [= q TOP
forall x:a, forall y:b, p (x,y) [= q (x,y)
------------------------------------------ product induction principle
            forall xy:a*b, p xy [= q xy

                p TOP [= q TOP
                p BOT [= q BOT
forall x:a, p (inl x) [= q (inl x)
forall y:b, p (inr y) [= q (inr y)
---------------------------------- sum induction principle
  forall xy:a+b, p xy [= q xy

            p TOP [= q TOP
-------------------------- TOP induction principle
forall x:TOP, p x [= q x

             p TOP [= q TOP
             p BOT [= q BOT
               p K [= q K    
               p F [= q F    
--------------------------- bool induction principle
forall b:bool, p b [= q b

                   p TOP [= q TOP
                   p BOT [= q BOT
                  p zero [= q zero      
forall n:nat, p (succ n) [= q (succ n)
-------------------------------------- nat induction principle
       forall n:nat, p n [= q n

The reasoning principles developed here are intended to be used in the Pomagma forward-chaining inference engine (see a.theory and types.theory in the Pomagma project).

References

License

Copyright (c) 2014-2015 Fritz Obermeyer.
All code is released under the Apache 2.0 License.