Other Peoples Thoughts

"i kinda like haskell and erlang but i don't think they make it any easier to do anything. by the time you learn how to do the one liners, time has passed and you've become a professor of computer science, and your applications no longer matter."

"wow lisp occured in 1958"

"Yeah, but Haskell does such nice things for you. Like pattern matching? Very mathematical feel"

regarding C: "damn it.I m doing something so simple and its takes time.its like traveling from the UK to France via China"

Common Subexpression Elimination

;; My example of when mutation is a useful tool that simplifies things.

(define (identity i) i)
(define (concat xs) (apply append xs))
(define (concat-map f x) (concat (map f x)))
(define (sort by xs)
  (define (insert by x xs)
    (if (null? xs)
        (list x)
        (if (< (by x) (by (car xs)))
            (cons x xs)
            (cons (car xs) (insert by x (cdr xs))))))
  (if (null? xs) '()
      (insert by (car xs) (sort by (cdr xs)))))

;; <variadic-tree> ::= <leaf> | (<variadic-tree> ...)
;; <leaf> is any non-list datum

(define (leaf? datum) (not (list? datum)))

(define (variadic-tree leaf nodes)
  (lambda (tree)
    (if (leaf? tree)
        (leaf tree)
        (apply nodes (map (variadic-tree leaf nodes) tree)))))

(define copy-tree (variadic-tree identity list))

(define exp-1
  (copy-tree
   '(+ (* (- x-1 x-2) (- x-1 x-2))
       (* (- y-1 y-2) (- y-1 y-2))
       (* (- z-1 z-2) (- z-1 z-2)))))

(define (splat tree)
  (if (leaf? tree)
      '()
      (cons tree (concat-map splat tree))))

(define (subexpressions tree) (sort length (cdr (splat tree))))

(define (eliminate exp sub sym)
  (cond ((null? exp) exp)
        ((leaf? exp) exp)
        ((cond ((equal? sub (car exp)) (set-car! exp sym))
               (else (eliminate (car exp) sub sym)))
         (eliminate (cdr exp) sub sym)
         exp)))

(define gensym
  (let ((n 0))
    (lambda ()
      (set! n (+ n 1))
      (string->symbol (string-append "g" (number->string n))))))

(define (eliminate-subexpressions env exp subs)
  (cond ((null? subs) `(let ,(reverse env) ,exp))
        (else
         (let* ((g (gensym))
                (sub (car subs))
                (exp-2 (eliminate exp sub g)))
           (eliminate-subexpressions (cons (list g sub) env) exp-2 (subexpressions exp-2))))))

;; (eliminate-subexpressions '() exp-1 (subexpressions exp-1))
;; =>
;; (let ((g1 (- z-1 z-2))
;;       (g2 (* g1 g1))
;;       (g3 (- y-1 y-2))
;;       (g4 (* g3 g3))
;;       (g5 (- x-1 x-2))
;;       (g6 (* g5 g5)))
;;   (+ g6 g4 g2))

Virgin Killer

http://www.theregister.co.uk/2008/12/07/brit_isps_censor_wikipedia/

http://iwfwebfilter.thus.net/error/blocked.html


You are currently unable to edit pages on Wikipedia.

You can still read pages, but cannot edit, change, or create them.

Editing from 193.195.3.41 (your account, IP address, or IP address range) has been disabled by Lucasbfr for the following reason(s):

193.195.3.41 <-- This is the IP of the filter which I view wikipedia through.



I am not able to edit wikipedia because one of the million people viewing it through the same ip filter as me vandalised as article and was banned. I found out this censorship was the reason. Maybe if you want to help abused children you could find a way that doesn't mean sitting in a comfy chair fiddling with 1's and 0's and patting yourself on the back.


Statement by "IWF":

"IWF statement regarding Wikipedia URL
IWF is the UK’s internet ‘Hotline’ for the public and IT professionals to report potentially illegal online content within our remit. We work in partnership with the online industry, law enforcement, government, the education sector, charities, international partners and the public to minimise the availability of this content, specifically, child sexual abuse content hosted anywhere in the world and criminally obscene and incitement to racial hatred content hosted in the UK. We are an independent self-regulatory body, funded by the EU and the wider online industry, including internet service providers, mobile operators and manufacturers, content service providers, filtering companies, search providers, trade associations and the financial sector as well as other organisations that support us for corporate social responsibility reasons.

We help internet service providers and hosting companies to combat abuse of their networks through our national ‘notice and take-down’ service which alerts them to potentially illegal content within our remit on their systems and we provide unique data to law enforcement partners in the UK and abroad to assist investigations into the distributers of potentially illegal online content. As sexually abusive images of children are primarily hosted abroad, we facilitate the industry-led initiative to protect users from inadvertent exposure to this content by blocking access to it through our provision of a dynamic list of child sexual abuse URLs.

A Wikipedia web page, was reported through the IWF’s online reporting mechanism in December 2008. As with all child sexual abuse reports received by our Hotline analysts, the image was assessed according to the UK Sentencing Guidelines Council (page 109). The content was considered to be a potentially illegal indecent image of a child under the age of 18, but hosted outside the UK. The IWF does not issue takedown notices to ISPs or hosting companies outside the UK, but we did advise one of our partner Hotlines abroad and our law enforcement partner agency of our assessment. The specific URL (individual webpage) was then added to the list provided to ISPs and other companies in the online sector to protect their customers from inadvertent exposure to a potentially illegal indecent image of a child."


I had not realized that wikipedia (The free encylcopedia) is a hive of child sexual abuse and a den for pedophiles.



to IWF: Wikipedia is a website for people that are like to read and learn things, studying, or writing. You are not helping the world or sexually abused children by censoring it. Realize you have become robots and by following your protocols you're actually worsening the planet for everyone.



This is how all Authoritarian/Stalinist governments work.
First they choose to censor something that most people would find reasonable to censor, such as the image of a naked child.
Before you know it, all wikipedia pages relating to opposition politicians and opposition parties will also be unavailable.
I see IWF are 'supported' by both the Home Office and the Dept of Business, Enterprise and Regulatory Reform, enough said !


For people like Berlusconi the world will always be open and free. He can get on a jet and talk to his friends in Australia in person. For the rest of us, the internet will be what Berlusconi and his ilk allow us to have and see. And yes this is a small step, but there have been hundreds of little steps that add up.

Axiom Free NoConfusion in Coq

Require Import Cast.
Require Import Fin.

Ltac prove_noConfusion :=
  intros;
    match goal with Eql : ?x = _ |- _ =>
      elim Eql; elim x; simpl; tauto end.

(*
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
*)

Definition NoConfusion_nat (P : Type) (x y : nat) : Type :=
  match x, y with
    | O, O => P -> P
    | O, S y => P
    | S x, O => P
    | S x, S y => (x = y -> P) -> P
  end.

Definition noConfusion_nat (P : Type) (x y : nat) :
  x = y -> NoConfusion_nat P x y.
prove_noConfusion.
Defined.

Definition eq_nat_dec : forall x y : nat, {x = y} + {x <> y}.
decide equality.
Defined.

Definition eq_nat_dec' : forall x y : nat, x = y \/ x <> y.
decide equality.
Defined.

(*
Inductive Fin : nat -> Set :=
| fz : forall n, Fin (S n)
| fs : forall n, Fin n -> Fin (S n).
*)

Notation FinINeq f g := (INeq nat Fin _ f _ g).

Definition NoConfusion_Fin (P : Type) (i : nat) (x y : Fin i) : Type :=
  match x, y with
    | fz _, fz _ => P -> P
    | fz _, fs _ _ => P
    | fs _ _, fz _=> P
    | fs x_i x, fs y_i y => (FinINeq x y -> P) -> P
  end.

Definition noConfusion_Fin (P : Type) (i : nat) (x y : Fin i) :
  x = y -> NoConfusion_Fin P i x y.
prove_noConfusion.
Defined.

Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)
  : fz = fs f -> P
  := fun Eq =>
    noConfusion_Fin P (S n) (fz) (fs f) Eq.

Definition fs_inj {n} {f f' : Fin n}
  : fs f = fs f' -> f = f'
  := fun Eq =>
    noConfusion_Fin (f = f') _ _ _ Eq (INeq_eq nat Fin eq_nat_dec _ _ _).

Inductive type : Set :=
| Nat : type
| Arrow : type -> type -> type.

Definition eq_type_dec (s t : type) : { s = t } + { s <> t }.
decide equality.
Defined.

Section equand.

Variable vars : nat.

Inductive equand : type -> Set :=
| Zero : equand Nat
| Succ : equand (Arrow Nat Nat)
| VAR (V : Fin vars) : equand Nat
| APP {A B} : equand (Arrow A B) -> equand A -> equand B.

Notation equandINeq f g := (INeq type equand _ f _ g).

Definition NoConfusion_equand (P : Type) (i : type) (x y : equand i) : Type :=
  match x, y with
    | Zero, Zero => P -> P
    | Succ, Succ => P -> P
    | VAR f, VAR f' => (f = f' -> P) -> P
    | APP xi xj xf xo, APP yi yj yf yo =>
      (equandINeq xf yf -> equandINeq xo yo -> P) -> P
    | _, _ => P
  end.

Definition noConfusion_equand (P : Type) (i : type) (x y : equand i) : x = y -> NoConfusion_equand P i x y.
prove_noConfusion.
Defined.

Definition Zero_One_clash (P : Type) (i : type)
  : Zero = APP Succ Zero -> P
  := fun Eq =>
    noConfusion_equand P Nat Zero (APP Succ Zero) Eq.

Definition APP_f_inj (u v : type) (F F' : equand (Arrow u v)) (O O' : equand u)
  : @APP u v F O = @APP u v F' O' -> F = F'
  := fun Eq =>
    noConfusion_equand (F = F') _ _ _ Eq
    (fun FEq OEq => INeq_eq _ _ eq_type_dec _ _ _ FEq).

Definition APP_o_inj (u v : type) (F F' : equand (Arrow u v)) (O O' : equand u)
  : @APP u v F O = @APP u v F' O' -> O = O'
  := fun Eq =>
    noConfusion_equand (O = O') _ _ _ Eq
    (fun FEq OEq => INeq_eq _ _ eq_type_dec _ _ _ OEq).

Definition eq_equand_dec : forall (t : type)(u v : equand t), {u = v} + {u <> v}.
apply INeq_dec_dec.
apply eq_type_dec.

refine (fix eq_equand_dec (i : type) (I : equand i)
                          (i' : type) (I' : equand i') {struct I} :
                          {@INeq _ _ i I i' I'} + {~ @INeq _ _ i I i' I'} := _).
refine (match I as I in equand i, I' as I' in equand i'
        return {@INeq _ _ i I i' I'} + {~ @INeq _ _ i I i' I'}
        with
          | Zero, Zero => _
          | Zero, Succ => _
          | Zero, VAR _ => _
          | Zero, APP _ _ _ _ => _
          | Succ, Zero => _
          | Succ, Succ => _
          | Succ, VAR _ => _
          | Succ, APP _ _ _ _ => _
          | VAR _, Zero => _
          | VAR _, Succ => _
          | VAR _, VAR _ => _
          | VAR _, APP _ _ _ _ => _
          | APP _ _ _ _, Zero => _
          | APP _ _ _ _, Succ => _
          | APP _ _ _ _, VAR _ => _
          | APP _ _ _ _, APP _ _ _ _ => _
        end);

try solve [ discriminate
          | left; reflexivity
          | right; intro Q; inversion Q
          | destruct B; right; intro Q; inversion Q; discriminate
          ].

destruct (fin_eq_dec V V0); subst.
left; reflexivity.
right; intro Q; inversion Q; contradiction.

destruct (eq_type_dec B B0);
(destruct (eq_equand_dec _ e0 _ e2) as [Q|N];[inversion Q|idtac]);
(destruct (eq_equand_dec _ e _ e1) as [Q'|N'];[inversion Q'|idtac]);
  subst;

try solve [ left;
  rewrite Q; try apply eq_type_dec;
  rewrite Q'; try apply eq_type_dec;
    reflexivity ];

right; intro NQ;
  try inversion NQ;
  try inversion Q;
  try inversion Q';
  try contradiction;
  try subst;
  try pose (APP_f_inj _ _ _ _ _ _ (INeq_eq _ _ eq_type_dec _ _ _ NQ));
  try pose (APP_o_inj _ _ _ _ _ _ (INeq_eq _ _ eq_type_dec _ _ _ NQ)).

apply N'; rewrite e3; reflexivity.
apply N; rewrite e4; reflexivity.
apply N; rewrite e4; reflexivity.
Defined.

Eval compute in (eq_equand_dec _
  (APP Succ (APP Succ Zero))
  (APP Succ (APP Succ Zero))
).

End equand.

Print Assumptions eq_equand_dec.


(*
 *  = left (APP Succ (APP Succ Zero) = APP Succ (APP Succ Zero) -> False)
 *      (refl_equal (APP Succ (APP Succ Zero)))
 *  : {APP Succ (APP Succ Zero) = APP Succ (APP Succ Zero)} +
 *    {APP Succ (APP Succ Zero) <> APP Succ (APP Succ Zero)}
 *
 * Computed fully, no JMeq_eq axiom stopping reduction
 *
 *)

Require Import Coven.
Require Import Arith.
Require Import Omega.
Print le.

Lemma le_irrelevent : forall n m (H1 H2:le n m), H1=H2.
refine (fix le_irrelevent n m (H1 H2:le n m) {struct H1} : H1=H2 := _).
apply INeq_eq; auto with arith.

refine (
  match H1 as H1' in _ <= m', H2 as H2' in _ <= m''
  return m = m' ->
         m = m'' ->
         INeq nat (le n) m H1 m' H1' ->
         INeq nat (le n) m H2 m'' H2' ->
         INeq nat (le n) m H1 m H2
  with
    | le_n, le_n => fun m'eq m''eq H1eq H2eq => _
    | le_n, le_S p_m p_le => fun m'eq m''eq H1eq H2eq => !
    | le_S p_m p_le, le_n => fun m'eq m''eq H1eq H2eq => !
    | le_S p_m p_le, le_S p_m' p_le' => fun m'eq m''eq H1eq H2eq => _
  end
  (refl_equal _)
  (refl_equal _)
  (INeq_refl _ _ _ _)
  (INeq_refl _ _ _ _)
); subst; subst.

rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H1eq).
rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H2eq).
reflexivity.

omega.

omega.

injection m''eq; intro; subst.
rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H1eq).
rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H2eq).
rewrite (le_irrelevent _ _ p_le p_le').
reflexivity.
Qed.

Print Assumptions le_irrelevent.
(** Closed under the global context **)

Dependently typed Data.Dynamic

Require Import Eqdep_dec_defined.

Section Cast.
  
  Variable U:Type.
  Variable F : U -> Type.
  
  Variable eq_dec : forall x y:U, {x = y} + {x <> y}.
  
  Definition eq_decide : forall x y:U, x = y \/ x <> y.
  intros x y; destruct (eq_dec x y); [ left | right ]; assumption.
  Defined.
  
  Definition cast (i j : U) : F j -> option (F i) :=
    fun J =>
      match eq_dec j i with
        | left Eql => match Eql in _ = i return option (F i) with
                        | refl_equal => Some J
                      end
        | right _ => None
      end.
  
  Theorem cast_reflexivity (i : U) (I : F i) : cast i i I = Some I.
    unfold cast; intro i; destruct (eq_dec i i);
      [ subst | absurd (i = i); tauto ].
    rewrite (eq_proofs_unicity eq_decide e (refl_equal i)).
    reflexivity.
  Defined.
  
  Definition cast_injective (i : U) (I I' : F i) :
    cast i i I = cast i i I' -> I = I'.
  intros i I I'; repeat rewrite cast_reflexivity.
  intro SomeEq; injection SomeEq; tauto.
  Defined.
  
  Inductive INeq (i : U)(I : F i) : forall (j : U)(J : F j), Prop :=
  | INeq_refl : INeq i I i I.
  Implicit Arguments INeq [i j].
  
  Hint Resolve INeq_refl.
  
  Definition INeq_eq (i : U)(I I' : F i) : INeq I I' -> I = I'.
  intros i I I' inEq; apply cast_injective.
  change ((fun i' I' => cast i i I = cast i i' I') i I').
  elim inEq; reflexivity.
  Defined.
  Implicit Arguments INeq_eq [i I I'].
  
  Lemma INeq_ind_r :
    forall (i:U) (I J:F i) (P:F i -> Prop), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Lemma INeq_rec_r :
    forall (i:U) (I J:F i) (P:F i -> Set), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Lemma INeq_rect_r :
    forall (i:U) (I J:F i) (P:F i -> Type), P J -> INeq I J -> P I.
    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.
  Defined.
  
  Definition INeq_dec_dec :
    (forall (i:U)(I:F i) (j:U)(J:F j), {INeq I J} + {~INeq I J}) ->
    (forall (i:U)(I J:F i), {I = J} + {I <> J}).
  intros ineq_dec i I J; destruct (ineq_dec i I i J); [ left | right ].
  apply INeq_eq; assumption.
  contradict n; subst; reflexivity.
  Defined.
  
End Cast.