Executable BNF parser in Prolog

% <digit> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
% <sign> ::= + | -
% <number> ::= [ <sign> ] <digit> { <digit> }


:- op(1120, xfx, ::=).
:- op(11, fx, <), op(13, xf, >).


<digit>  ::= 0 ; 1 ; 2 ; 3 ; 4 ; 5 ; 6 ; 7 ; 8 ; 9 .
<sign>   ::= (+) ; (-)                             .
<number> ::= [ <sign> ], <digit>, { <digit> }      .

<expr>   ::= <factor>, { ((+) ; (-)), <factor> }   .
<factor> ::= <term>,   { ((*) ; (/)), <term> }     .
<term>   ::= '(', <expr>, ')' ; <number>           .


parse(Rule)    --> { Rule ::= Body }, parse(Body).
parse(Atom)    --> { atomic(Atom), atom_codes(Atom, Codes) }, Codes.

parse((X , Y)) --> parse(X), parse(Y).

parse((X ; _)) --> parse(X).
parse((_;Y;Z)) --> parse(Y ; Z).
parse((_ ; Z)) --> { Z \= (_ ; _) }, parse(Z).

parse([X])     --> parse(X).
parse([_])     --> {}.

parse({X})     --> parse(X), parse({X}).
parse({_})     --> [].


% phrase(parse(<expr>), "-5*(73+7)").

Compare with a C implementation -- http://cvs.savannah.gnu.org/viewvc/bnf/bnf/src/grio.c?view=markup

An Embedded ALGOL-like language in Prolog

%% Embedded ALGOL-like language in Prolog

change_member(_, N, [], [N]).
change_member(O, N, [O|XS], [N|XS]).
change_member(O, N, [X|XS], [X|YS]) :- change_member(O, N, XS, YS).


:- op(900, xfy, :=).
:- op(100, fx, [if, then, else]).
:- op(125, fx, [while,  return]).
:- op(125, yfx, do).


run({Block},                          EnvI, O, Ret) :-
  run(Block, EnvI, O, Ret).

run((First; Second),                  EnvI, O, Ret) :-
  run(First, EnvI, M, _), run(Second, M, O, Ret).

run(Place := Expr,                    EnvI, O, void) :-
  eval(Expr, Value, EnvI), change_member(Place = _, Place = Value, EnvI, O), !.

run(if(Cond) then {This} else {That}, EnvI, O, Ret) :-
  eval(Cond, Value, EnvI),
  ( Value = true -> Body = This ; Body = That ),
  run(Body, EnvI, O, Ret).

run(while(Cond) do {Body},            EnvI, O, Ret) :-
  eval(Cond, Value, EnvI),
  ( Value = true -> run(Body, EnvI, M, _),
                    run(while(Cond) do {Body}, M, O, Ret)
  ; O = EnvI, Ret = void
  ).

run(return Value,                     EnvI, O, Ret) :-
  eval(Value, Ret, EnvI), O = EnvI.


eval(Var,   Val,   Env) :- member(Var = Val, Env), !.
eval(Num,   Num,   _  ) :- number(Num), !.
eval(true,  true,  _  ).
eval(false, false, _  ).

eval(X + Y, Z, Env) :- eval(X, XV, Env), eval(Y, YV, Env), Z is XV + YV.
eval(X - Y, Z, Env) :- eval(X, XV, Env), eval(Y, YV, Env), Z is XV - YV.
eval(X * Y, Z, Env) :- eval(X, XV, Env), eval(Y, YV, Env), Z is XV * YV.
eval(X / Y, Z, Env) :- eval(X, XV, Env), eval(Y, YV, Env), Z is truncate(XV / YV).

eval(X = Y, B, Env) :- eval(X, XV, Env), eval(Y, YV, Env),
  ( XV = YV -> B = true ; B = false ).
eval(X < Y, B, Env) :- eval(X, XV, Env), eval(Y, YV, Env),
  ( XV < YV -> B = true ; B = false ).
eval(X > Y, B, Env) :- eval(X, XV, Env), eval(Y, YV, Env),
  ( XV > YV -> B = true ; B = false ).
eval(not(P), B, Env) :- eval(P, PV, Env),
  ( PV = true -> B = false ; B = true ).





factorial(N, {i := 1;
              n := N;
              while(n > 0) do {
                i := i * n;
                n := n - 1
              };
              return i}).

%% ?- factorial(5, P), run(P, [], _, X).

%% X = 120



fibonacci(F, {i := 1; a := 1; b := 1;
              while(not(i = F)) do {
                a := a + b;
                b := a - b;
                i := i + 1
              };
              return b}).

%% ?- fibonacci(7, P), run(P, [], _, X).

%% X = 13



pow2(N, {i := N;
         n := 1;
         while(not(i = 0)) do {
           i := i - 1;
           n := n * 2
         };
         return n}).

%% ?- pow2(8, P), run(P, [], _, X).

%% X = 256



gcd(X, Y,
    {x := X;
     y := Y;
     while(not(x = 0)) do {
       if(x < y) then {
         y := y - x
       }
       else {
         x := x - y
       }
     };
     return y}).

%% ?- A is 2*2*5*7*13, B is 5*13*7*7, gcd(A, B, P), run(P, [], _, X).

%% A = 1820,
%% B = 3185,
%% X = 455



isqrt(N, {q := N; p := (q + N / q) / 2;
          while(q > p) do {
            q := p;
            p := (q + N / q) / 2
          };
          return p}).

%% ?- isqrt(81, P), run(P, [], _, X).

%% X = 9

Proof of the foldl, foldr relation

-- This is a self contained development of the proof that
--  foldr f z (reverse xs) ≡ foldl (flip f) z xs

-- I use some definitions from
-- http://code.haskell.org/~dolio/agda-play/
-- Particularly Data.List and Relation.Equivality

module Folding where

flip : forall {A B C} -> (A -> B -> C) -> B -> A -> C
flip f b a = f a b


infix  20 _≡_
infixr 30 _≡→_
infixr 25 _lhs_ _rhs_

data _≡_ {a : Set} : a -> a -> Set where
  refl : forall {x} -> x ≡ x

≡sub : forall {a}{P : a -> Set}{x y : a} -> x ≡ y -> P x -> P y
≡sub refl Px = Px

≡symm : forall {a}{x y : a} -> x ≡ y -> y ≡ x
≡symm refl = refl

≡trans : forall {a}{x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z
≡trans refl refl = refl

-- take and equation and apply a function to both sides
_≡→_ : forall {a b}{x y : a} -> x ≡ y -> (f : a -> b) -> f x ≡ f y
refl ≡→ _ = refl

-- rewrite on the left
_lhs_ : forall {a}{x y k : a} -> x ≡ k -> x ≡ y -> y ≡ k
E₁ lhs E₂ = ≡trans (≡symm E₂) E₁

-- rewrite on the right
_rhs_ : forall {a}{x y k : a} -> k ≡ x -> x ≡ y -> k ≡ y
E₁ rhs E₂ = ≡symm (≡symm E₁ lhs E₂)


infixr 50 _∷_ 
infixr 40 _++_

data [_] (a : Set) : Set where
  [] : [ a ]
  _∷_ : a -> [ a ] -> [ a ]


foldr : {a b : Set} -> (a -> b -> b) -> b -> [ a ] -> b
foldr _ z []       = z
foldr f z (a ∷ as) = f a (foldr f z as)

foldl : {a b : Set} -> (b -> a -> b) -> b -> [ a ] -> b
foldl _ z []       = z
foldl f z (a ∷ as) = foldl f (f z a) as

_++_ : forall {a} -> [ a ] -> [ a ] -> [ a ]
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

reverse : {A : Set} -> [ A ] -> [ A ]
reverse []       = []
reverse (x ∷ xs) = reverse xs ++ (x ∷ [])


-- Some theorems about ++

-- [] is the right unit
++unit : forall {a} -> (x : [ a ]) -> x ++ [] ≡ x
++unit []       = refl
++unit (x ∷ xs) = ++unit xs ≡→ \s -> x ∷ s

-- Associative
++assoc : forall {a} -> (a b c : [ a ]) ->
   (a ++ b) ++ c ≡ a ++ (b ++ c)
++assoc {_} []       _ _ = refl
++assoc {_} (x ∷ xs) _ _ = ++assoc xs _ _ ≡→ \s -> x ∷ s

++reverse : forall {a} (x y : [ a ]) ->
   reverse y ++ reverse x ≡ reverse (x ++ y)
++reverse [] ys       = ++unit (reverse ys)
++reverse (x ∷ xs) ys = ++reverse xs ys
                        ≡→ (\s -> s ++ reverse (x ∷ []))
                        lhs ++assoc (reverse ys) _ _

++foldr : forall {a b} ->
          (f : a -> b -> b) -> (z : b) -> (xs ys : [ a ]) ->
   foldr f z (xs ++ ys) ≡ foldr f (foldr f z ys) xs
++foldr f z []       ys = refl
++foldr f z (x ∷ xs) ys = ++foldr f z xs ys ≡→ f x

-- This identity is not actually used but I leave it in for
-- the sake of completeness
++foldl : forall {a b} ->
          (f : b -> a -> b) -> (z : b) -> (xs ys : [ a ]) ->
   foldl f z (xs ++ ys) ≡ foldl f (foldl f z xs) ys
++foldl f z []       ys = refl
++foldl f z (x ∷ xs) ys = ++foldl f (f z x) xs ys


foldl^foldr : forall {a b} ->
              (f : a -> b -> b) -> (z : b) -> (xs : [ a ]) ->
   foldr f z (reverse xs) ≡ foldl (flip f) z xs
foldl^foldr f z []       = refl
foldl^foldr f z (x ∷ xs) = foldl^foldr f (f x z) xs
                           lhs ≡symm (++foldr f z
                                              (reverse xs)
                                              (x ∷ []))

Type inference for The Simply Typed Lambda Calculus

%% Type inference for The Simply Typed Lambda Calculus

:- op(150, xfx, ⊢).
:- op(140, xfx, :).
:- op(100, xfy, ->).
:- op(100, yfx, $).

Γ ⊢    Term : Type          :- atom(Term), member(Term : Type, Γ).
Γ ⊢ λ(A, B) : Alpha -> Beta :- [A : Alpha|Γ] ⊢ B : Beta.
Γ ⊢   A $ B : Beta          :- Γ ⊢ A : Alpha -> Beta, Γ ⊢ B : Alpha.

/** Examples:

% Typing fix
?- Γ ⊢ y $ f : Y, Γ ⊢ f $ (y $ f) : Y.
Γ = [y: (Y->Y)->Y, f:Y->Y|_G330]

% Typing the Y combinator
?- Γ ⊢ λ(f, (λ(f,f $ f)) $ (λ(g,f $ (g $ g)))) : Y.
Y = (_G309 -> _G309) -> _G309 

% Typing flip id
?- Id = λ(i, i), Flip = λ(f, λ(y, λ(x, f $ x $ y))),
   Γ ⊢ Flip $ Id : T.
T = _G395 -> (_G395 -> _G411) -> _G411

**/

Gödel's beta function

I read a most incredible proof in the book, Lectures On The Curry Howard Isomorphism that I decided to created a program from it.

(defun factorial (n)
  (if (= n 0) 1
      (* n (factorial (- n 1)))))

(defun extended-euclidean-algorithm (a b)
  ;; function extended_gcd(a, b)
  ;;  if (a mod b = 0)
  ;;     return {0, 1}
  ;;  else {x, y} := extended_gcd(b, a mod b)
  ;;       return {y, x-y*(a div b)}
  (if (= (mod a b) 0) (values 0 1)
      (multiple-value-bind (x y) 
          (extended-euclidean-algorithm b (mod a b))
        (values y (- x (* y (floor a b)))))))

(defun extended-euclidean-algorithm-prime (a b)
  ;; extended-euclidean-algorithm solves:
  ;;  u*a + v*b = gcd
  ;; This one solves:
  ;;  u*a - v*b = gcd
  (multiple-value-bind (u v)
      (extended-euclidean-algorithm a b)
    (if (= b 1)
        (values 1 (- a 1))
        (values u (- v)))))

;; For every finite sequence k_0, k_1, ..., k_r there exist two numbers m, n, such that (β m n j) = k_j, for j = 0..r.
(defun β (m n j)
  (mod m (+ (* n (+ j 1)) 1)))

;; Produce n m, such that (β m n j) = k_j
(defun β-solve (k)
  (let* ((n (factorial (apply #'max (- (length k) 1) k)))
         (a (loop for j below (length k) collect (+ (* n (+ j 1)) 1))))
    (labels ((next-m (l m)
               (if (= l (- (length k) 1)) m
                   (let ((a* (apply #'* (subseq a 0 (min (+ l 1) (length k))))))
                     (multiple-value-bind (u v)
                         (extended-euclidean-algorithm-prime (elt a (+ l 1)) a*)
                       (declare (ignore u))
                       (next-m (+ l 1)
                               (+ m (* (* (- m (elt k (+ l 1))) v) a*))))))))
      (values (next-m 0 (elt k 0)) n))))


;; CL-USER> (multiple-value-bind (n m)
;;              (β-solve (map 'list #'char-code "You win!"))
;;            (map 'string #'code-char (loop for j below 8 collect (β n m j))))
;; "You win!"

Counting Infinity

import Data.List
import Data.Ratio

-- A few utilities and toys for later:

data Void                    {- This needs -XEmptyDataDecls -}
instance Show Void

data Tree = N | Tree :@: Tree deriving Show

-- interleaving append
a      +~~+ []     = a
[]     +~~+ b      = b
(a:as) +~~+ (b:bs) = a : b : as +~~+ bs

diagonalZipWith f as bs = [ f a b
                          | (x,y) <- pairs
                          , a <- as !! x
                          , b <- bs !! y ]
  where []     !! _ = []
        (x:_)  !! 0 = [x]
        (_:xs) !! n = xs !! (n-1)

(*) `on` f = \x y -> f x * f y




-- We shall get started with some basic infinite sets of numbers

nats = [0..]
-- [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,..]

ints = 0 : [1..] +~~+ map negate [1..]
-- [0,1,-1,2,-2,3,-3,4,-4,5,-5,6,-6,7,-7,8,-8,9,-9,10,-10,11,-11,..]

primes = nubBy(((>1).).gcd)[2..]
-- [2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,..]
-- (My thanks to the author of this whoever you are (: )

fibs = map fst $ iterate (\(x,y)->(y,x+y)) $ (0,1)
-- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377,610,987,1597,2584,4181,..]




-- Looking at the diagonals of every pair of nats:
--
--   (0,0) (1,0) (2,0) (3,0)
--   (0,1) (1,1) (2,1) (3,1)
--   (0,2) (1,2) (2,2) (3,2)
--   (0,3) (1,3) (2,3) (3,3)
--
-- Each element of the first diagonal, having one element, sums to zero,
-- Each element of the second, two of them, sums to one, ...

pairs = concatMap pairsSummingTo [0..]
  where pairsSummingTo n = map (\i -> (i, n-i)) [0..n]
-- [(0,0),(0,1),(1,0),(0,2),(1,1),(2,0),(0,3),(1,2),(2,1),(3,0),(0,4),
--  (1,3),(2,2),(3,1),(4,0),(0,5),(1,4),(2,3),(3,2),(4,1),(5,0),(0,6),
--  (1,5),(2,4),(3,3),(4,2),(5,1),(6,0),(0,7),(1,6),...]




-- Let us consider every unique rational, They all (a%b) have GCD(a,b) = 1
-- Let's then, start with the GCD 1 and execute Euclid's algorithm backwards.

{-
 - i: 1%1 in Q
 - f: a%b in Q -> (a+b)%b in Q
 - g: a%b in Q -> a%(a+b) in Q
 -}

{- [{I}, {FI}, {GI}, {FFI}, {FGI}, {GFI}, {GGI}, {FFFI}, ...] -}
{- concat [[{I}], [{FI}, {GI}], [{FFI}, {FGI}, {GFI}, {GGI}],
           [{FFFI}, ...], ...] -}

rationals = let rats   0   = [i]
                rats (n+1) = map f (rats n) ++ map g (rats n)
             in concatMap rats nats
  where i   = 1%1
        f r = (numerator r + denominator r) % denominator r
        g r = numerator r % (numerator r + denominator r)
-- [1%1,2%1,1%2,3%1,3%2,2%3,1%3,4%1,5%2,5%3,4%3,3%4,3%5,2%5,1%4,5%1,7%2,
--  8%3,7%3,7%4,8%5,7%5,5%4,4%5,5%7,5%8,4%7,3%7,3%8,2%7,...]





-- Every string that can be made from a list of symbols
strings symbols = concat [ enumerate n symbols | n <- [1..] ]
  where enumerate 0 _ = [""]
        enumerate n d = concatMap (\y->map (:y) d) (enumerate (n-1) d)


-- Every binary sequence
binary = strings ['1', '0']
-- ["1","0","11","01","10","00","111","011","101","001","110",
--  "010","100","000","1111","0111","1011","0011","1101","0101",
--  "1001","0001","1110","0110","1010","0010","1100","0100","1000",...]


-- This is a very slow method to generate all well parenthesized expressions
-- It is a perfectly valid method for proving that a set is enumerable though
-- In general, showing that a set is the subset of all strings composed from
-- some symbols
parenthesized = filter balanced $ strings ['(', ')']
  where split s = map (flip splitAt s) [1..length s-1]
        balanced []     = True
        balanced (_:[]) = False
        balanced s      =     head s == '(' && last s == ')'
                           && balanced (tail $ init $ s)
                        || any (uncurry ((&&) `on` balanced)) (split s)
-- ["()","()()","(())","()()()","(())()","()(())","(()())","((()))",
--  "()()()()","(())()()","()(())()","(()())()","((()))()","()()(())",
--  "(())(())","()(()())","(()()())","((())())","()((()))","(()(()))",
--  "((()()))","(((())))",...]



-- This is fabulous, So I stole it from:
-- http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/spigot.pdf
pi = g(1,180,60,2) where 
  g(q,r,t,i) = let (u,y)=(3*(3*i+1)*(3*i+2),div(q*(27*i-12)+5*r)(5*t)) 
               in y : g(10*q*i*(2*i-1),10*u*(q*(5*i-2)+r-y*t),t*u,i+1)
-- [3,1,4,1,5,9,2,6,5,3,5,8,9,7,9,3,2,3,8,4,6,2,6,4,3,3,8,3,2,7,9,5,0,...]




-- We can use typeclasses to recurse over the structure of a type
-- If a function listing all inhabitants of a type is written,
-- One can be sure that infinity will crop up.

class Inhabitants a where
  inhabitants :: [a]

instance Inhabitants Void where
  inhabitants = []

instance Inhabitants () where
  inhabitants = [()]

instance Inhabitants Bool where
  inhabitants = [True, False]

instance Inhabitants Integer where
  inhabitants = ints

instance Inhabitants a => Inhabitants (Maybe a) where
  inhabitants = [Nothing] ++ map Just inhabitants

instance (Inhabitants a, Inhabitants b) => Inhabitants (Either a b) where
  inhabitants = map Left inhabitants +~~+ map Right inhabitants

instance Inhabitants a => Inhabitants [a] where
  inhabitants = [[]] ++ diagonalZipWith (:) inhabitants inhabitants

instance Inhabitants Tree where
  inhabitants = [N] ++ diagonalZipWith (:@:) inhabitants inhabitants

-- take 600 $ inhabitants :: [ Either [Maybe Integer] Tree ]
--                             ^^ You can try various types here
--                                as long as they are in the
--                                Inhabitants class.