Commit 923b1fd5 authored by Uwe Köckemann's avatar Uwe Köckemann

Initial commit

parents
temp/
__pycache__/
*~
#*#
.#*
*#
#*
.pyc
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
#+TITLE: The AIDDL Common Library
The AIDDL Common Library contains type definitions, implementations and test
cases for many common AI algorithms. These implementations can be used as
building blocks for fast prototyping of integrated AI systems.
(#mod self org.aiddl.common)
(#nms EVAL "eval.aiddl")
(#def Map
(and
(type #self {list set})
(forall ?e #self
(and
(type ?e key-value) ))))
(#def MapGen
(match (?KT ?VT) #self
^(lambda ?M ($MapOf (?KT ?VT ?M)))))
(#def MapOf
(match (?KeyType ?ValueType ?Map) #self
(and
(type ?Map {^list ^set})
(forall ?k:?v ?Map
(and
(type ?k ?KeyType)
(type ?v ?ValueType)
)))))
(#def SetGen
^(lambda ?Set
($SetOf #self ?Set) ))
(#def (SetOf ?Type ?Set)
(and
(type ?Set ^set)
(forall ?e ?Set (type ?e ?Type))))
(#def ListGen
^(lambda ?List
(ListOf ?List #self) ))
(#def (ListOf ?Type)
(and
(type #self ^list)
(forall ?e #self (type ?e ?Type))))
(#def Composite
(match (?S ?Arg) #self
(and
(type ?S ^collection)
(forall ?e ?S (type ?Arg ?e))
)))
(#def KeyValuedType
^(lambda ?x
(forall ?k:?t #self
(call ?t (get-key ?k ?x))) ))
(#mod self org.aiddl.common.domain)
;; Finite sets of values & expressions that can be expanded into finite sets.
;; Domains are sets of key-values that attach value sets to types. Signatures
;; attach types to tuples (t1 t2 t3) or key-value pairs (t1 t2 t3):t4 This can
;; be used to limit the scope of legal assignments of atomics in logic or
;; state-variable assignments in planning.
(#namespace EVAL "eval.aiddl")
(#def EnumValues
(and
(type #self {#set #list})
(forall ?e #self
(type ?e { #symbolic #numerical #variable #string $DomainValues } )) ))
(#def IntegerValues
(and
(type #self #set)
(type (get min ?R) #integer)
(type (get max ?R) #integer) ))
(#def RationalValues
(and
(type #self #set)
(type (get min #self) #rational)
(type (get inc #self) #rational)
(>= (get inc #self) 0/1)
(type (get max #self) #rational) ))
(#def RealValues
(and
(type (get min #self) #real)
(type (get inc #self) #real)
(>= (get inc #self) 0.0)
(type (get max #self) #real) ))
(#def NumericalValues
(and
(type #self {
$IntegerDomain
$RealDomain
$RationalDomain})))
(#def TupleValues
(and
(type #self #tuple)
(forall ?e #self
(type ?e {symbolic $Domain}) )))
(#def KeyValueValues
(and
(type #self #key-value-pair)
(type (key #self) {symbolic $Domain})
(type (value #self) {symbolic $Domain}) ))
(#def DomainValues
(type #self
{ $Enum
$Numerical
$Tuple
$KeyValue }))
(#def Domains
(and
(type #self ^collection)
(forall ?X:?D #self
(and
(type ?D $DomainValues)))))
(#def TupleSignature
(and
(type #self ^tuple)
(forall ?e #self
(type ?e { ^symbolic } ) )))
(#def StateVariableSignature
(and
(type #self key-value)
(type (key #self) { ^$TupleSignature } )
(type (value #self) { ^symbolic } ) ))
(#def Signatures
(and
(type #self ^set)
(forall ?e #self (type ?e ^$TupleSignature ^$StateVariableSignature))))
(#mod self org.aiddl.common.learning.decision-tree)
(#nms EVAL org.aiddl.eval)
(#def Comparator (in #self {= < > >= <=}))
(#def Condition
(and
(type #self tuple)
(signature #self [$Comparator term term])))
(#def Decision
(and
(type #self tuple)
(signature #self [$Condition $DecisionTree])))
(#def DecisionTree
(or
(type #self #term)
(and
(type #self #list)
(forall ?e #self (type ?e Decision))
)))
(#mod self org.aiddl.common.learning.supervised)
(#nms EVAL org.aiddl.eval)
(#req T org.aiddl.common.domain)
(#req LA org.aiddl.common.math.linear-algebra)
(#def WildcardDomain
(= #self *))
(#def Attribute
(and
(type #self #tuple)
(signature #self [term {Domain@T $WildcardDomain}])))
(#def Attributes
(and
(type #self list)
(forall ?e #self
(type ?e $Attribute))))
(#def DataPoint (and (type #self list)))
(#def DataPoints
(and
(type #self {list set})
(forall ?e #self
(type ?e $DataPoint))))
(#def Problem
(and
(type #self tuple)
(match (attributes : ?Attributes label : ?Label data : ?Data) #self
(and
(type ?Attributes $Attributes)
(type ?Data $DataPoints)
(exists (?Label _) ?Attributes true)
(forall ?Datapoint ?Data
(and
(= (size ?Datapoint) (size ?Attributes))
(zip (?Att ?Val) [?Attributes ?Datapoint]
(match (?Var ?Domain) ?Att
(or
(= ?Domain *)
(in ?Val ?Domain)
)
)
)
)
)
)
)))
(#def ConfusionMatrix
(match (attributes : ?A matrix : ?M) #self
(and
(type ?A #list)
(type ?M Matrix@LA)
(= (size ?A) (size ?M))
(= (size ?A) (size (first ?M)))
)))
\ No newline at end of file
(#mod self org.aiddl.common.math.graph)
(#nms EVAL org.aiddl.eval)
(#req C org.aiddl.common)
;; Todo:
;; - Graph types (directed, ...)
;; -> Assemble from args? (Graph {directed weighted multi labeled})
(#def Node
(type #self ^term))
(#def Edge
(or
(type #self ^$UndirectedEdge)
(type #self ^$DirectedEdge) ))
(#def Label
(type #self ^term))
(#def UndirectedEdge
(and
(type #self {^tuple ^list ^set})
(type (get-key e #self) ^set)
(= (size (get-key e #self)) 2)
(forall ?e (get-key e #self)
(type ?e ^$Node) )))
(#def DirectedEdge
(and
(type #self {^tuple ^list ^set})
(exists e:?e #self
(and
(type ?e ^tuple)
(signature ?e [^$Node ^$Node])
(= (size ?e) 2) ))))
(#def LabeledEdge
(and
(type #self ^$Edge)
(exists label:?L #self
(type ?L ^$Label) )))
(#def WeightedEdge
(and
(type #self ^$Edge)
(exists w:?w #self
(type ?w ^numerical) )))
(#def Graph (type (^$Node ^$Edge #self) ^$TypedGraph))
(#def TypedGraph
(match (?NodeType ?EdgeType ?G) #self
(and
(type ?G ^tuple)
(match (V:?V E:?E) ?G
(and
(type ?V {^set ^list})
(forall ?v ?V (call ?NodeType ?v)) ;; (type ?v ?NodeType))
(forall ?e ?E
(and
(call ?EdgeType ?e) ;; (type ?e ?EdgeType)
(cond
(type ?e ^$UndirectedEdge) :
(contains-all ?V (get-key e ?e))
(type ?e ^$DirectedEdge) :
(and
(contains ?V (get-idx 0 (get-key e ?e)))
(contains ?V (get-idx 1 (get-key e ?e))) )))))))))
(#def Simple
(type (get-key V #self) ^set))
(#def Multi
(type (get-key V #self) ^list))
(#def Directed
(forall ?e (get-key E #self)
(type ?e ^$DirectedEdge) ))
(#def Undirected
(forall ?e (get-key E #self)
(type ?e ^$UndirectedEdge) ))
(#def Weighted
(forall ?e (get-key E #self)
(type ?e ^$WeightedEdge) ))
(#def Connected
(forall ?v1 (get-key V #self)
(forall ?v2 (get-key V #self)
(or
(= ?v1 ?v2)
(exists ?e (get-key E #self)
(= (get-key e ?e) {?v1 ?v2}) )))))
(#def Path
(and
(type #self ^list)
(forall ?n #self (type ?n ^$Node))))
(#def DistanceMap
(and
(type #self ^collection)
(forall ?k:?v #self
(and
(type ?k ^$Node)
(type ?v ^numerical) ))))
(#def PredecessorMap
(and
(type #self ^collection)
(forall ?k:?v #self
(and
(type ?k ^$Node)
(type ?v ^$Node) ))))
(#interface transpose (
uri : org.aiddl.common.math.graph.transpose
input : ^$Graph
output : ^$Graph
))
(#interface bellman-ford (
uri : org.aiddl.common.math.graph.bellman-ford
input : (KeyValuedType@C [graph:^$Graph start:^$Node target:^$Node])
output : (KeyValuedType@C [path:^$Path distance:^$DistanceMap predecessor:^$PredecessorMap])
))
(#interface depth-first-search (
uri : org.aiddl.common.match.graph.depth-first-search
input : $Graph
output : (KeyValuedType@C [
pi:^(MapGen@C ^$Node ^$Node)
distances:^(MapGen ^$Node ^numerical)
finish-times:^(MapGen@C ^$Node ^numerical)
components:^(SetGen@C ^(SetGen@C ^$Node)) ]
)
))
(#interface strongly-connected-components (
uri : org.aiddl.common.math.graph.scc-computer
input : ^$Graph
output : ^(SetGen@C ^(SetGen@C ^$Node))
))
\ No newline at end of file
(#mod self org.aiddl.common.math.linear-algebra)
(#nms EVAL org.aiddl.eval)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Real and Complex Numbers
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(#def Complex (and (type #self ^tuple) (signature ^#real ^real) (size equals 2)))
(#def Field (type #self {^numerical ^$Complex}))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Vectors, Matrices, and linear Equations
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(#def Vector
(and
(type #self ^tuple)
(signature #self [^$Field])))
(#def Matrix
(and
(type #self ^tuple)
(forall ?e #self
(and
(type ?e ^$Vector)
(= (size ?e) (size (first #self)))
))))
(#mod self org.aiddl.common.planning.state-variable.data)
(#nms E org.aiddl.eval)
(#req P org.aiddl.common.planning.state-variable)
(#req FL org.aiddl.common.reasoning.logic.first-order)
;; (#def RelaxedPlanningGraph
;; (and
;; (type #self list)
;; (forall ?idx (domain {min:0 max:(- (size #self) 1)})
;; (let [?L:(get-idx ?idx #self)]
;; (and
;; (type ?L set)
;; (if (= (modulo ?idx 2) 0)
;; (forall ?e ?L
;; (or
;; (type ?e Atom@FL)
;; (type ?e StateVariableAssignment@P)))
;; (forall ?e ?L
;; (type ?e Operator@P) )))))))
(#def RelaxedPlanningGraph
(and
(type #self ^list)
(let
[?O:(reduce
(lambda (?c ?x) (union {(get-idx ?x #self) ?c}))
(filter (lambda ?x (= (modulo ?x 2) 1)) (domain {min:0 max:(- (size #self) 1)}))
initial-value:{})
?P:(reduce (lambda (?c ?x) (union {(get-idx ?x #self) ?c}))
(filter (lambda ?x (= (modulo ?x 2) 0)) (domain {min:0 max:(- (size #self) 1)}))
initial-value:{})]
(and
(forall ?e ?P
(type ?e ^StateVariableAssignment@P))
(forall ?e ?O
(type ?e ^Operator@P) )))))
(#interface rpg-creator (
uri : (sym-concat $self rpg-creator)
input : ^Problem@P
output : ^$RelaxedPlanningGraph
))
(#mod self org.aiddl.common.planning.hierarchical-task-network)
(#req C org.aiddl.common)
(#req G org.aiddl.common.math.graph)
(#req FOL org.aiddl.common.reasoning.logic.first-order)
(#req SVP org.aiddl.common.state-variable)
(#def Task (type #self Atom@FOL))
(#def TotallyOrderedTaskNetwork
(type #self (List $Task)@C))
(#def DigraphTaskNetwork
(type #self (Graph $Task DirectedEdge@G)@G))
(#def TaskNetwork
(or
(type #self $TotallyOrderedTaskNetwork)
(type #self $DigraphTaskNetwork)
))
(#def SimpleTaskNetworkMethod
(and
(type #self #tuple)
(let [
?N : (get-key name #self)
?T : (get-key task #self)
?P : (get-key preconditions #self)
?S : (get-key subtasks #self) ]
(and
(type ?N Atom@FL)
(type ?T $Task)
(type ?P $StateVariableAssignments)
(type ?S $TaskNetwork)
))))
(#def HtnMethod NIL)
(#def Constraints NIL)
\ No newline at end of file
(#mod self org.aiddl.common.planning.plan-space)
(#def Action NIL)
(#def CausalLink NIL)
(#def OrderingConstraint NIL)