## Thursday, 31 January 2008

### 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**/`

## Sunday, 27 January 2008

### 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!"`

## Wednesday, 23 January 2008

### Counting Infinity

`import Data.Listimport Data.Ratio-- A few utilities and toys for later:data Void                    {- This needs -XEmptyDataDecls -}instance Show Voiddata Tree = N | Tree :@: Tree deriving Show-- interleaving appenda      +~~+ []     = a[]     +~~+ b      = b(a:as) +~~+ (b:bs) = a : b : as +~~+ bsdiagonalZipWith 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 numbersnats = [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 symbolsstrings symbols = concat [ enumerate n symbols | n <- [1..] ]  where enumerate 0 _ = [""]        enumerate n d = concatMap (\y->map (:y) d) (enumerate (n-1) d)-- Every binary sequencebinary = 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 symbolsparenthesized = 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.pdfpi = 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 = intsinstance Inhabitants a => Inhabitants (Maybe a) where  inhabitants = [Nothing] ++ map Just inhabitantsinstance (Inhabitants a, Inhabitants b) => Inhabitants (Either a b) where  inhabitants = map Left inhabitants +~~+ map Right inhabitantsinstance Inhabitants a => Inhabitants [a] where  inhabitants = [[]] ++ diagonalZipWith (:) inhabitants inhabitantsinstance 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.`

### XOR Encryption

`#include <stdio.h>#include <stdlib.h>FILE * input,     * key,     * output;int main(void) {  input  = fopen("in.txt",  "r");  key    = fopen("key.txt", "r");  output = fopen("out.txt", "w");    if(!input)  { puts("input failure");  return EXIT_FAILURE; }  if(!key)    { puts("key failure");    return EXIT_FAILURE; }  if(!output) { puts("output failure"); return EXIT_FAILURE; }    while(!feof(input))    { if(feof(key)) rewind(key); fputc(fgetc(input) ^ fgetc(key), output); }    return EXIT_SUCCESS;}`

### Generate, Test and Intertwine

`%% Generate, Test and Intertwine%% -----------------------------%% The aim here is to generate 4x4 magic squares. First of all, We start%% with the 3x3 case, since that's easier.%% This way any improvements can be reused, assuming they are general enough%% I'll define a magic square as, an nxn table of numbers such that all the%% rows, columns and diagonals sum to the same value, each number in the range%% 1 .. n^2 appears once in the grid.%% In Prolog, We'll represent squares as lists:%: [4,8,2,%:  3,5,7,%:  8,1,6]%% So to generate this, We'll select numbers from a list of digits and insert%% them into the table and check that everything adds up.saturn_digits([1,2,3,4,5,6,7,8,9]).saturn([A,B,C,        D,E,F,        G,H,I]) :-        saturn_digits(D1),        select(A, D1, D2),        select(B, D2, D3),        select(C, D3, D4),        select(D, D4, D5),        select(E, D5, D6),        select(F, D6, D7),        select(G, D7, D8),        select(H, D8, D9),        select(I, D9, []),        S is A + B + C,        S is D + E + F,        S is G + H + I,        S is A + D + G,        S is B + E + H,        S is C + F + I,        S is A + E + I,        S is C + E + G.%% That first attempt works fine:%? ?- saturn(Square).%? Square = [2, 7, 6, 9, 5, 1, 4, 3, 8] ;%? Square = [2, 9, 4, 7, 5, 3, 6, 1, 8] ;%? Square = [4, 3, 8, 9, 5, 1, 2, 7, 6] ;%? Square = [4, 9, 2, 3, 5, 7, 8, 1, 6] ;%? Square = [6, 1, 8, 7, 5, 3, 2, 9, 4] ;%? Square = [6, 7, 2, 1, 5, 9, 8, 3, 4] ;%? Square = [8, 1, 6, 3, 5, 7, 4, 9, 2] ;%? Square = [8, 3, 4, 1, 5, 9, 6, 7, 2] ;%% It's quite clear the program is correct,%% The two important properties are%%  * Soundness -- Generates only magic squares%%  * Completeness -- Generates every magic square%%%% Since digits are selected from the list, It's possible for the square to%% be filled in every possible way, and due to:%:   select(I, D9, []),%% It's ensured that every digit is used. Every row, column and diagonal is%% summed, since S is used for all summations, this ensures that all the sums%% are equal.%% There is this pattern in the code though, which I don't very much like:%: select(A, D1, D2),%: select(B, D2, D3),%: select(C, D3, D4),%: select(D, D4, D5),%: select(E, D5, D6),%: select(F, D6, D7),%: select(G, D7, D8),%: select(H, D8, D9),%: select(I, D9, []),%% Prolog has a macro, DCG style, that lets us erase this pattern.%% If we use --> instead of :- , then this is implicit, everything is sewn%% together like we did manually, except automatically.%% {} is used to escape it.%% So now, It can be rewritten to the equivalent program:saturn_2([A,B,C,          D,E,F,          G,H,I]) -->        select(A),        select(B),        select(C),        select(D),        select(E),        select(F),        select(G),        select(H),        select(I),        { S is A + B + C },        { S is D + E + F },        { S is G + H + I },        { S is A + D + G },        { S is B + E + H },        { S is C + F + I },        { S is A + E + I },        { S is C + E + G }.%? ?- saturn_digits(D), saturn_2(Square, D, []).%? D = [1, 2, 3, 4, 5, 6, 7, 8, 9],%? Square = [2, 7, 6, 9, 5, 1, 4, 3, 8] ;%? ..%% It produces all the same answers in the same order. One of the fantastic%% thing about Prolog is you could actually implement DCG in it, if it wasn't%% already there, Or even your own macros.%% Anyway, there is an optmisation which is quite blatant: select always%% succeeds, It's the tests in {} which cause backtracking, So if we were to%% intertwine the generating (done by select) with the testing, (as done by%% summation) then backtracking which does occur, will happen sooner.saturn_3([A,B,C,          D,E,F,          G,H,I]) -->        select(A),        select(B),        select(C),        { S is A + B + C },        select(D),        select(G),        { S is A + D + G },        select(E),        { S is C + E + G },        select(F),        { S is D + E + F },        select(H),        { S is B + E + H },        select(I),        { S is G + H + I },        { S is C + F + I },        { S is A + E + I }.%% So now, It's straightforward to use the same process for the 4x4 case.%% We use DCG first in this case though.jupiter_digits([1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]).jupiter([A,B,C,D,         E,F,G,H,         I,J,K,L,         M,N,O,P]) -->        select(A),        select(B),        select(C),        select(D),        select(E),        select(F),        select(G),        select(H),        select(I),        select(J),        select(K),        select(L),        select(M),        select(N),        select(O),        select(P),                { S is A + B + C + D },        { S is E + F + G + H },        { S is I + J + K + L },        { S is M + N + O + P },                { S is A + E + I + M },        { S is B + F + J + N },        { S is C + G + K + O },        { S is D + H + L + P },                { S is A + F + K + P },        { S is D + G + J + M }.%% And then rearrangejupiter_2([A,B,C,D,           E,F,G,H,           I,J,K,L,           M,N,O,P]) -->        select(A),        select(B),        select(C),        select(D),        %% * * * *        %% o o o o        %% o o o o        %% o o o o        { S is A + B + C + D },                select(E),        select(I),        select(M),        %% * * * *        %% * o o o        %% * o o o        %% * o o o        { S is A + E + I + M },                select(F),        select(K),        select(P),        %% * * * *        %% * * o o        %% * o * o        %% * o o *        { S is A + F + K + P },                select(G),        select(H),        %% * * * *        %% * * * *        %% * o * o        %% * o o *        { S is E + F + G + H },                select(L),        %% * * * *        %% * * * *        %% * o * *        %% * o o *        { S is D + H + L + P },                select(J),        %% * * * *        %% * * * *        %% * * * *        %% * o o *        { S is I + J + K + L },        { S is D + G + J + M },                select(N),        %% * * * *        %% * * * *        %% * * * *        %% * * o *        { S is B + F + J + N },                select(O),        %% * * * *        %% * * * *        %% * * * *        %% * * * *        { S is M + N + O + P },        { S is C + G + K + O }.%? ?- jupiter_digits(D), jupiter_2(Square, D, []).%? %? D = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16],%? Square = [1, 2, 15, 16, 12, 14, 3, 5, 13, 7, 10, 4, 8, 11, 6, 9] ;%? ...%% There is a huge speed difference in the two versions.%% Here's the final program without comments:jupiter_3([A,B,C,D,           E,F,G,H,           I,J,K,L,           M,N,O,P]) -->        select(A),        select(B),        select(C),        select(D),        { S is A + B + C + D },        select(E),        select(I),        select(M),        { S is A + E + I + M },        select(F),        select(K),        select(P),        { S is A + F + K + P },        select(G),        select(H),        { S is E + F + G + H },        select(L),        { S is D + H + L + P },        select(J),        { S is I + J + K + L },        { S is D + G + J + M },        select(N),        { S is B + F + J + N },        select(O),        { S is M + N + O + P },        { S is C + G + K + O }.`