LU Decomposition in Prolog

:- use_module(library(clpr)).

// various obvious bits of matrix machinary.

lu_decompose(M, L*U) :-
 dimensions(M,N*N),
 dimensions(L,N*N),
 dimensions(U,N*N),
 lower(L),
 upper(U),
 matrix_multiply(L,U,M).

ZFC's probably inconsistent

Now stop worrying and enjoy your life.

Nice books

Cantors Diagonalization Proof in Coq

Axiom b : (nat -> nat) -> nat.
Axiom b' : nat -> (nat -> nat).

Axiom bijection : forall f, b' (b f) = f.
Axiom bijection' : forall x, b (b' x) = x.

Definition Stream A := nat -> A.
Definition Map {A B} (f : A -> B) : Stream A -> Stream B :=
  fun sa =>
    fun i =>
      f (sa i).

Definition l : Stream (nat -> nat) -> Stream nat :=
  Map b.
Definition l' : Stream nat -> Stream (nat -> nat) :=
  Map b'.

Definition isnt x :=
  match x with
    | O => S O
    | S _ => O
  end.

Theorem isn't_isnt {x} : isnt x <> x.
  destruct x; discriminate.
Qed.

Definition Diagonal {A} (s : Stream (Stream A)) : Stream A:=
  fun i => s i i.

Definition Diagonalization (sequences : Stream (nat -> nat)) : Stream nat :=
  Map isnt (Diagonal sequences).

Theorem isn't_in {sequences} : forall i, Diagonalization sequences <> sequences i.
intros; intro.
pose (f_equal (fun f => f i) H) as H'.
unfold Diagonalization in H'.
unfold Diagonal in H'.
unfold Map in H'.
revert H'.
apply isn't_isnt.
Qed.

Definition pink_elephant : Stream nat := fun i => i.

Definition sequence_enumeration : Stream (nat -> nat) := l' pink_elephant.

Theorem every_sequence : forall s, exists i, s = sequence_enumeration i.
intro s; exists (b s).
unfold sequence_enumeration.
unfold pink_elephant.
unfold l'.
unfold Map.
rewrite bijection.
reflexivity.
Qed.

Theorem Cantor : False.
destruct (every_sequence (Diagonalization sequence_enumeration)) as [i iPrf].
pose (@isn't_in sequence_enumeration i).
contradiction.
Qed.

Short Note on Semantics

With all curious derivations that come from the forests of To Mock a Mockingbird, and in the intrests of deepening understanding of type theory (in particular CIC) we considered axiomatizing the SK calculus in Coq.

Module Type SK.
  (* axiomatization of the theory *)
  Parameter SK : Set.

  Parameter app : SK -> SK -> SK.
  Infix "*" := app.
  
  Parameter S : SK.
  Parameter K : SK.
  
  Axiom S_prop : forall a b c, S * a * b * c = (a * c) * (b * c).
  Axiom K_prop : forall a b, K * a * b = a.
End SK.

It is not defined as an inductive type (as you might usually do) because there is no normal form for SK that we can compute terms into inside Coq (we would have to equate diverging terms with an "omega" symbol for a start, which is well known to be a partial operation). It would be possible to use a non-normal forma and quotient it out with a special (undecidable) equivalence relation, but we do not this.. Instead the axioms of the theory are given, One immediately notices that there is a trivial model of these axioms:

Module SK_trivial_model : SK.
  (* one model (giving non-contradiction of the theory) *)
  Definition SK := unit.
  
  Definition app := fun (_ _ : unit) => tt.
  Infix "*" := app.
  
  Definition S := tt.
  Definition K := tt.
  
  Theorem S_prop : forall a b c, S * a * b * c = (a * c) * (b * c).
    reflexivity.
  Qed.
  
  Theorem K_prop : forall a b, K * a * b = a.
    destruct a; reflexivity.
  Qed.
End SK_trivial_model.

(This implementation mostly serves to show the syntax and so on of how to construct a model of a theory inside Coq).

Anyway, we eliminate trivial models by saying that S <> K.

  Axiom SK_prop : S <> K.

We could now develop the theory of combinator calculus, prove things like S <> I and so forth.

Module SK_theory <: SK.
  Include Type SK.
  
  (* Development of the theory of SK calculus, valid for all models *)
  
  Ltac sk := repeat (rewrite S_prop || rewrite K_prop).
  
  Definition I := S * K * S.
  Theorem I_prop : forall x, I * x = x.
    intros; unfold I; sk; reflexivity.
  Qed.
  Ltac ski := repeat (sk || rewrite I_prop).
  
  Theorem IK : I <> K.
    Definition F x y b := b * K * I * x * y.
    
    intro Eq; generalize (f_equal (F K S) Eq); unfold F; ski.
    apply SK_prop.
  Qed.
  
  Definition U := S * I * I.
  Theorem U_prop : forall x, U * x = x * x.
    intros; unfold U; ski; reflexivity.
  Qed.
  
  Ltac skiu := repeat (ski; rewrite U_prop).
End SK_theory.

As fun as that would be, I don't believe you could ever reach a contradiction by assuming the SK theory. Yet no model exists inside Coq!

This is a rather confusing and troubling state, but Russell O'Connor mentioned to me the possibility of giving an interpretation of CIC into a theory that has a Halting-Oracle and that solves it! This is surely a valid interpretation of CIC, it's just got this SK theory added in with the usual stuff - the halting oracle would be used to normalize SK terms and prove satisfy our theory. So despite the non-existence of a model of SK inside Coq: It appears we can reason about the SK calculus directly. (Rather than a halting oracle you might have considered a special equivalence relation being interpreted for the congruence of SK objects but lets pretend Coq has Axiom K so that need not be considered).

This is all very interesting to me because it seems to suggest mathematics existing outside of the formal theory we work in or study. Something I never believed in - It's not completely clear if this is profound or if I am just going soft.

Do you live in UK?

http://www.pirateparty.org.uk/

Strongly Specified Parser Combinators

Following the approach Wouter Swierstra used for Hoare State Monad, we define a Parser monad with pre and post conditions that express soundness (but not completeness) of the parser.

The computational aspect of it is the same old parser monad, type Parser s a = [s] -> [(s, [a])], which takes a list of tokens [s] to a (possibly empty) list (here is where backtracking/nondeterminism comes into it) of parses paired with the rest of the text. It's a monad and also a monad plus.

On the specification end, we can put a precondition on the input string (for example, you might say the input length is <= some value, for ensuring termination of a recursive parser) and also a post condition comparing the input with the parsed value and the remaining output.

  Definition Pre := list s -> Prop.
  Definition Post (t : Set) := list s -> t -> list s -> Prop.
  
  Program Definition Parser (pre : Pre) (t : Set) (post : Post t) : Set :=
      forall i : { t : list s | pre t }, list ({ (x, r) : t * list s | post i x r }).

in Haskell we might define:

m >>= f = \i -> concatMap (uncurry f) (m i)

And in Coq, using Program we have roughly the same thing. Except that one has to apply a 'noncomputational_map' to fudge the proofs paired up with the list elements.

  Program Definition Bind (a b : Set) P1 P2 Q1 Q2
    (m : Parser P1 a Q1)
    (f : (forall x : a, Parser (P2 x) b (Q2 x))) :
    Parser (fun i => P1 i /\ forall x o, Q1 i x o -> P2 x o)
           b
           (fun i x' o' => exists x o, Q1 i x o /\ Q2 x o x' o') :=
    fun i => @flat_map ({ (x, o) : a * list s | Q1 i x o }) _
      (fun xo => match xo with (x,o) => noncomputational_map _ _ _ _ (f x o) end)
      (m i).

Seeing as noncomputational map doesn't do anything, we prove a theorem expressing that as justification for extracting it out as the identity function (rather it being equivalent to map id traversing the whole list).

  Theorem noncomputational_map_identity :
    forall l,
      map (@proj1_sig _ _) l = map (@proj1_sig _ _) (noncomputational_map l).
  
  Extract Inlined Constant noncomputational_map => "id".

Another nice parser combinator is the fixed point of a parser:

  Program Definition Fix t {P Q} :
    (forall i : { t : list s | P t },
      Parser (fun i' => length i' < length i /\ P i') t Q ->
      list ({ (x, o) : t * list s | Q i x o })) ->
    Parser P t Q :=
    fun Rec =>
      well_founded_induction
        (well_founded_ltof ({ i : list s | P i }) (fun i => length i))
        (fun i => list ({ (x, o) : t * list s | Q i x o }))
        (fun x Rec' => Rec x (fun i => Rec' i _)).

It packages up well founded recursion on the size of the input string, so that any non-left recursive parsers should be easily defined.

Enough of the heavy machinary! A simple example of putting thing into work now:

 <par> ::= <epsilon> | '(' <par> ')' <par>

To parse this we define a type of tokens and abstract syntax of parsing derivations - then relate them with a function:

  Inductive token := open | close.
  Inductive par := epsilon : par | wrappend : par -> par -> par.

  Fixpoint print (p : par) : list token :=
    match p with
      | epsilon => nil
      | wrappend m n => (open::nil) ++ print m ++ (close::nil) ++ print n
    end.

Now Program lets us define the par parser as the fixed point of the sum of epsilon and wrapped recursions:

  Program Definition par_parser : Parser token (fun _ => True) par (fun x p y => x = print p ++ y /\ length y <= length x) :=
    Fix token par (fun i parRec =>
      Plus _ _ (fun i' => i = i') _
        (fudge_pre_and_post_conditions _ _ _
          (Return epsilon))
        (fudge_pre_and_post_conditions _ _ _
          (Symbol token eq_token_dec open >>= fun _ =>
           parRec >>= fun m =>
           Symbol token eq_token_dec close >>= fun _ =>
           parRec >>= fun n =>
           Return (wrappend m n)))
      i).

Here are the actual scripts http://github.com/odge/parseq/tree/master