狠狠撸

Veri?ed Stack-based
Genetic Programming
via Dependent Types
by Larry Diehl

Tuesday, July 19, 2011

Motivation
? avoid searching space of stack under/
over?owing programs
? use strongly typed genetic operators
? avoid logic and runtime errors due to
increasingly complex genetic operators
? use a total and dependently typed
language


Dependent Types
? Agda programming language
? purely functional (like Haskell)
? total (coverage/termination/positivity)
? types can encode any intuitionistic logic
formula
? e.g. proof theory judgement “Even 6”

Genetic Programming

? representation
? genetic operators
? evaluation function
? initialization procedure


“Forth” operations

word consumes produces
true 0 1
not 1 1
and 2 1


“Forth” terms

1→1 3→1 0→1 7→7 6→4 0→3
not and not and true
not and not and true
true true


append (ill)
1
and
and
2 ≠ 3
not
true
true
0


append (ill)
2
and
2 ≠ 3
not
true
true
0


append (well)
1
and 1
2 = 2 and
not not
true true
true true
0 0


split
1
1 and
and 2 = 2
not not
true true
true true
0 0


split
1
and
2 not
and true
not 1 = 1
true true
true 0
0


Agda Crash Course


data Bool : Set where
true false : Bool

data ? : Set where
zero : ?
suc : ? ! ?

one : ?
one = suc zero

two : ?
two = suc one

three : ?
three = suc two


data List (A : Set) : Set where
[] : List A
_∷_ : A ! List A ! List A

false∷[] : List Bool
false∷[] = false ∷ []

true∷false∷[] : List Bool
true∷false∷[] = true ∷ false∷[]


data Vec (A : Set) : ? ! Set where
[] : Vec A zero
_∷_ : {n : ?} !
A ! Vec A n ! Vec A (suc n)

false∷[]1 : Vec Bool one
false∷[]1 = false ∷ []

true∷false∷[]2 : Vec Bool two
true∷false∷[]2 = true ∷ false∷[]1


_+_ : ? ! ? ! ?
zero + n = n
suc m + n = suc (m + n)

_++_ : {A : Set} {m n : ?} !
Vec A m ! Vec A n ! Vec A (m + n)
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

true∷false∷true∷[]3 : Vec Bool three
true∷false∷true∷[]3 =
(true ∷ false ∷ []) ++ (true ∷ [])


Representation


data Word : Set where
true not and : Word

data List (A : Set) : Set where
[] : List A

_∷_ : A ! List A ! List A

Term = List Word


bc : Term -- 2 1
bc = and ∷ []

ab : Term -- 0 2
ab = not ∷ true ∷ true ∷ []

ac : Term -- 0 1
ac = and ∷ not ∷ true ∷ true ∷ []


bc : Term 2 1
bc = and []

ab : Term 0 2
ab = not (true (true []))

ac : Term 0 1
ac = and (not (true (true [])))


data Term (inp : ?) : ? ! Set where
[] : Term inp inp
true : {out : ?} !
Term inp out !
Term inp (1 + out)
not : {out : ?} !
Term inp (1 + out) !
Term inp (1 + out)
and : {out : ?} !
Term inp (2 + out) !
Term inp (1 + out)


module DTGP
{Word : Set}
(pre post : Word ! ? ! ?)
where

data Term (inp : ?) : ? ! Set where
[] : Term inp inp

_∷_ : ? {n} (w : Word) !
Term inp (pre w n) !
Term inp (post w n)


true not and : Word

pre : Word ! ? ! ?
pre true n = n
pre not n = 1 + n
pre and n = 2 + n

post : Word ! ? ! ?
post true n = 1 + n
post not n = 1 + n
post and n = 1 + n

open import DTGP pre post


bc : Term 2 1
bc = and ∷ []

ab : Term 0 2

ac : Term 0 1


Genetic Operators


crossover : {inp out : ?}
(female male : Term inp out)
(randF randM : ?) !
Term inp out × Term inp out


bc : Term 2 1
bc = and ∷ []

ab : Term 0 2

ac : Term 0 1
ac = bc ++ ab


_++_ : ? {inp mid out} !
Term mid out !
Term inp mid !
Term inp out
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)


ac : Term 0 1

bc++ab : Split 2 ac
bc++ab = bc ++' ab


data Split {inp out} mid :
Term inp out ! Set where
_++'_ :
(xs : Term mid out)
(ys : Term inp mid) !
Split mid (xs ++ ys)


ac : Term 0 1

bc++ab : Split 2 ac
bc++ab = proj? (split 1 ac)


ac : Term 0 1

bc++ab : Σ ? λ mid ! Split mid ac
bc++ab = split 1 ac


split : ? {inp out} (n : ?)
(xs : Term inp out) !
Σ ? λ mid ! Split mid xs
split zero xs = _ , [] ++' xs
split (suc n) [] = _ , [] ++' []
split (suc n) (x ∷ xs) with split n xs
split (suc n) (x ∷ .(xs ++ ys))
| _ , xs ++' ys = _ , (x ∷ xs) ++' ys


Evaluation Function


bc : Term 2 1
bc = and ∷ []

eval-bc : Vec Bool 1
eval-bc = eval bc (true ∷ false ∷ [])

ac : Term 0 1

eval-ac : Vec Bool 1
eval-ac = eval ac []


eval : {inp out : ?} ! Term inp out !
Vec Bool inp ! Vec Bool out
eval [] is = is
eval (true ∷ xs) is = true ∷ eval xs is
eval (not ∷ xs) is with eval xs is
... | o ∷ os = ? o ∷ os
eval (and ∷ xs) is with eval xs is
... | o? ∷ o? ∷ os = (o? ∧ o?) ∷ os


score : Term 0 1 ! ?
score xs with eval xs []
... | true ∷ [] = 0
... | false ∷ [] = 1

open Evolution score


Initialization Procedure


choices : List Word
choices = true ∷ not ∷ and ∷ []

population : List (Term 0 1)
population = init 2 0 1 choices
-- (and ∷ true ∷ true ∷ []) ∷
-- (not ∷ not ∷ true ∷ []) ∷
-- (not ∷ true ∷ []) ∷
-- (true ∷ []) ∷
-- []


-- data Term (inp : ?) : ? ! Set where
-- _∷_ : ? {n} (w : Word) !
-- Term inp (pre w n) !
-- Term inp (post w n)
-- pre : Word ! ? ! ?
-- pre and n = 2 + n

true∷true : Term 0 2
true∷true = true ∷ true ∷ []

and∷and∷true : Term 0 1
and∷and∷true = _∷_ {n = 0} and true∷true


match : (w : Word) (out : ?) !
Dec (Σ ? λ n ! out ≡ pre w n)
match true n = yes (n , refl)
match not zero = no ?p where
?p : Σ ? (λ n ! 0 ≡ suc n) ! ⊥
?p (_ , ())
match not (suc n) = yes (n , refl)


match and zero = no ?p where
?p : Σ ? (λ n ! 0 ≡ suc (suc n)) ! ⊥
?p (_ , ())
match and (suc zero) = no ?p where
?p : Σ ? (λ n ! 1 ≡ suc (suc n)) ! ⊥
?p (_ , ())
match and (suc (suc n)) = yes (n , refl)

open Initialization match


Generalization


module DTGP
{Domain Word : Set}
(pre post : Word ! Domain ! Domain)
(_?_ : (x y : Domain) ! Dec (x ≡ y))
where

data Term (inp : Domain) : Domain ! Set where
[] : Term inp inp

_∷_ : ? {d} (w : Word) !
Term inp (pre w d) !
Term inp (post w d)


not gt : Word
num : ? ! Word

record Domain : Set where
constructor _,_
field
bools : ?
nats : ?

postulate _?_ :
(x y : Domain) ! Dec (x ≡ y)


pre : Word ! Domain ! Domain
pre not (m , n) = 1 + m , n
pre (num _) (m , n) = m , n
pre gt (m , n) = m , 2 + n

post : Word ! Domain ! Domain
post not (m , n) = 1 + m , n
post (num _) (m , n) = m , 1 + n
post gt (m , n) = 1 + m , n

open DTGP pre post _?_


bc : Term (0 , 2) (1 , 0)
bc = not ∷ gt ∷ []

ab : Term (0 , 0) (0 , 2)
ab = num 3 ∷ num 5 ∷ []

ac : Term (0 , 0) (1 , 0)
ac = bc ++ ab


FIN
github.com/larrytheliquid/dtgp/tree/aaip11
questions?


狠狠撸

DTGP AAIP11

More Related Content

Viewers also liked (7)

Recently uploaded (20)

DTGP AAIP11