Carnap @ TheEdu17

Graham Leach-Krouse

<gleachkr@ksu.edu>

Kansas State University

Interactive Slides available at:

gleachkr.github.io/CADEslides

Today

Description of The Project

What is it?

Carnap is an free and open framework for developing formal reasoning applications that run in a standard web browser

For example

Carnap aims to be modular, flexible, and generic

Beginning from an extensible higher-order abstract syntax, Carnap can generically perform operations like higher-order unification, semantic evaluation, and term-rewriting on realizations of this syntax.

Why would you make that?

Rudoph Carnap

“Let us grant to those who work in any special field of investigation the freedom to use any form of expression which seems useful to them; the work in the field will sooner or later lead to the elimination of those forms which have no useful function.

Let us be cautious in making assertions and critical in examining them, but tolerant in permitting linguistic forms.”

Minimize Barrier to Entry

Maximize Adaptability, Extensibility

Take Advantage of Modern Web Technologies

How do you make that?

Demonstrations

Language of Propositional Logic

In case that "essentially" makes you nervous:

Connectives (Generic)

Connectives (Boolean)

Sentence Letters (Generic)

Sentence Letters (Boolean)

We can make a lexicon (disjoint union) of symbol types thus:

type PropLexicon = Prop :|: Conn

Hiding some dark magic in that :|: operator.

But this isn't quite a language yet...

type PropLang = FixLang PropLexicon

Result:

:|-: (P\/-P)

How does the parser work?

We combine a generic parser for Prop a and a generic parser for Conn b

Non-generic part: Approximately 7 SLOC

How does the display work?

instance Schematizable Prop where
    schematize (Pred n) = λ_ -> "P" ++ show n

instance Schematizable Conn where
    schematize Not = λ(p:_) -> "¬" ++ p

Everything derived generically from these declarations.

How does the proof-checker work?

I lied ever so slightly about what's in the language. It also includes schematic sentence letters.

type PropLexicon = 
    Prop :|: Conn :|: SchematicProp

These are just letters like φ and ψ that usually occur in the statement of inference rules

Logics are specified by declarative rules.

On the board:

modus ponens is:
φ
(φ→ψ)
ψ

In the code:

modusPonens = 
    [ GammaV 1 ⊢ phi 1
    , GammaV 2 ⊢ (phi 1 .→. phi 2)
    ] ∴ (GammaV 1 :+: GammaV 2) ⊢ phi 2

What about a more complicated language?

Language of First-Order Logic 

type FirstOrderLexicon = PropLexicon
                     :|: FreeVar
                     :|: Pred 
                     :|: Quant 
                     :|: SchematicPred

Types of Quantifiers

All :: Quant ((Thing -> Bool) -> Bool)
Some :: Quant ((Thing -> Bool) -> Bool)

Result:

Ax(G(x)), Ax(G(x)->F(x)):|-: Ax(F(x))

Higher-Order Logic?

:|-: EXAy(X(y))

Fitch style proofs?

:|-: ((P->Q)->P)->P

Other Language Ingredients

Currently Available

Behind the Scenes

Unification

Proof checking is powered by an implementation of Huet's algorithm.

Huet is complete for higher-order unification problems (if there is a solution, Huet finds it)

Algorithm is non-deterministic, type-directed, and stateful. Haskell is very helpful here.

Higher-order unification is Σ₁-complete, therefore undecidable.

The problems encountered in Carnap's proof-checking are merelysecond-order pattern-matching, an (NP-complete) class decided by Huet.

Run time performace is (surprisingly) not bad.

Syntax

Implicit Fixed Point: 
data IntList = Nil | Cons Int (IntList)
Explicit Fixed Point (Just an example!): 
data PreList b = PreNil | PreCons Int b
data Fix f  = Fx (f (Fix f))
type List = Fix Prelist
pattern Nil = Fx PreNil
pattern Cons x y = Fx (PreCons x y)

Example Type Derivation

PreNil               :: PreList a b
→ Fx PreNil          :: Fix (Prelist a (Fix (Prelist a))
= Nil                :: List a
→ PreCons 5 Nil      :: Prelist Int (List Int)
→ Fx (PreCons 5 Nil) :: Fix (Prelist Int (List Int))
= Cons 5 Nil         :: List Int

Carnap's FixLang 

PropLexicon a b :: (Predicate Prop :|: ...) a b
data Fix f b = Fx (f (Fix f) b)
type FixLang f = Fix (Copula :|: f)

FixLang adds to explicit fix-point construction of an ADT:

  1. a type parameter for Carnap's phantom types, and
  2. the Copula type, which binds the language together.

Proof-Checking

  1. Each line is converted to a Genzen-Style proof tree, by tracing its "deductive pedigree".
  2. Proof Trees are folded from top to bottom, using Huet at each stage to check that premises and conclusions unify with the premises and conclusions of cited rules, and to compute dependencies.

Applications

Teaching Tool

So Far:

This Fall:

How did you use Carnap?

What's that like?

Very positive experience.

Student evaluations in top decile for university

Some predictable difficulties.

Planned Applications

Thank you!

Questions?

mailto:gleachkr@ksu.edu
irc://irc.freenode.net/carnap
https://gitter.im/Carnap-Prover