formal-logic

Formalisation of some logical systems, in Agda, Idris, and Haskell.

Notes

This work compares a number of techniques for formalising typed higher-order languages in a typed meta-language, with an eye towards the readability of programs written in the resulting object-language.

Following Troelstra and Schwichtenberg, we use M, I, and C for minimal, intuitionistic, and classical first-order predicate calculus, respectively; Mp, Ip, and Cp stand for the corresponding propositional systems. For technical reasons, we refer to minimal implicational logic as ArrMp, and to minimal implicational modal logic as BoxMp.

We investigate the issue of binder representation by contrasting the use of de Bruijn indices against parametric higher-order abstract syntax (PHOAS), after Chlipala. Each approach is presented in the widely-used initial encoding, using a generalised algebraic data type, and the final encoding of Carette, Kiselyov, and Shan, using a sequence of type classes.

We refer to the de Bruijn, vector-based de Bruijn, and PHOAS approach as B, V, and P, respectively; i and f correspond to the initial and final encoding.

Implementations

	Pi	Pf	Bi	Vi	Bf
ArrMp	agda, idr, hs	agda, idr, hs	agda	agda	agda
BoxMp	agda, idr, hs	agda, idr, hs	agda	agda	agda
Mp	agda, idr, hs	agda, idr, hs	agda	agda	agda
Ip	agda, idr, hs	agda, idr, hs	agda	agda	agda
Cp	agda, idr, hs	agda, idr, hs	agda	agda	agda
M	agda, idr
I	agda, idr
C	agda, idr

Usage

To check all files automatically:

$ make

To load a particular file for interactive use:

$ agda --safe -I -i src src/FILE.agda

$ ghci -Wall -isrc src/FILE.hs

$ idris -i src src/FILE.idr

Tested with Agda 2.4.2.3, Idris 0.9.19, and GHC 7.8.4.

Notation

This section describes the notation available in the PHOAS approach; in the de Bruijn approach, variable binding is not part of the constructors or eliminators.

Agda

Op	Type	Constructors	Eliminators
→	=>	lam v => e	e₁ $ e₂
∧	&&	[ e₁ , e₂ ]	fst e ; snd e
∨	`		`
⊥	FALSE	—	I: abort e ; C: abort v => e
↔︎	<=>	—	—
¬	NOT	—	—
⊤	TRUE	—	—
∀	FORALL	pi v => e	e₁ $$ e₂
∃	EXISTS	[ e₁ ,, e₂ ]	split e₀ as v => e
□	BOX	box e	unbox e₀ as v => e
◇	DIAMOND	—	—

Idris

Op	Type	Constructors	Eliminators
→	:=>	lam v :=> e	e₁ :$ e₂
∧	:&&	[ e₁ , e₂ ]	fst e ; snd e
∨	`:		`
⊥	FALSE	—	I: abort e ; C: abort v :=> e
↔︎	:<=>	—	—
¬	NOT	—	—
⊤	TRUE	—	—
∀	FORALL	pi v :=> e	e₁ :$$ e₂
∃	EXISTS	[ e₁ ,, e₂ ]	split e₀ as v :=> e
□	BOX	box e	unbox e₀ as v :=> e
◇	DIAMOND	—	—

Haskell

Op	Type	Constructors	Eliminators
→	:=>	lam λ	i: e₁ :$ e₂ ; f: e₁ .$ e₂
∧	:&&	pair ( e₁ , e₂ )	fst' e ; snd'  e
∨	`:		`
⊥	FALSE	—	I: abort e ; C: abort λ
↔︎	:<=>	—	—
¬	NOT	—	—
⊤	TRUE	—	—
∀	FORALL	pi λ	i: e₁ :$$ e₂ ; f: e₁ .$$ e₂
∃	EXISTS	sig ( e₁ , e₂ )	split e₀ λ
□	BOX	box e	unbox e₀ λ
◇	DIAMOND	—	—

About

Made by Miëtek Bak. Published under the MIT X11 license.

Thanks to Dominique Devriese, Darryl McAdams, and Andrea Vezzosi for comments and discussion.

References

• J.-P. Bernardy, PHOAS.hs, 2008
• G. Boolos, “The logic of provability”, 1993
• J. Carette, O. Kiselyov, C. Shan, “Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages”, 2009
• A. Chlipala, “Parametric higher-order abstract syntax for mechanized semantics”, 2008
• N.A. Danielsson, HOAS.SimplyTyped.agda, 2008
• D. Devriese, F. Piessens, “On the bright side of type classes: Instance arguments in Agda”, 2011
• F. Pfenning, R. Davies, “A judgmental reconstruction of modal logic”, 2001
• A.S. Troelstra, H. Schwichtenberg, “Basic proof theory”, 2000