%% 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

**/

## Thursday, 31 January 2008

### Type inference for The Simply Typed Lambda Calculus

## 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.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.

### 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 rearrange

jupiter_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 }.

Subscribe to:
Posts (Atom)