CONTEXT AST IN ENGLISH INCLUDE "Braga.xlsx" -- contains data -- Display in 24pt font. -- Display 12 lines at a time. -- Type Checking by -- Domain Analysis in Ampersand -- -- RAMICS 2015 -- -- Stef Joosten -- Sebastiaan Joosten -- This presentation: -- Rules in Ampersand -- Domain analysis -- -- This demonstration is in Ampersand -- For a Haskell implementation -- see the links in our paper PATTERN "Terms and Rules" -- A Rule prescribes that two terms are equal. -- e.g. "r = s;t", -- lhsTerm is the Term "r" -- and its rhsTerm is "s;t" RELATION lhsTerm[Rule*Term] [UNI,TOT] RELATION rhsTerm[Rule*Term] [UNI,TOT] -- Example: s;t is a BinaryTerm CLASSIFY BinaryTerm ISA Term RELATION first[BinaryTerm*Term] [UNI,TOT] RELATION second[BinaryTerm*Term] [UNI,TOT] CLASSIFY Composition ISA BinaryTerm CLASSIFY Intersection ISA BinaryTerm CLASSIFY Minus ISA BinaryTerm CLASSIFY Identity ISA Term CLASSIFY Full ISA Term CLASSIFY Converse ISA Term RELATION arg[Converse*Term] [UNI,TOT] CLASSIFY Relation ISA Term ENDPATTERN PATTERN "Types and concepts" RELATION source[Relation*Concept] [UNI] RELATION target[Relation*Concept] [UNI] RELATION src[Term*Concept] -- Is only [UNI] in type-correct scripts. We want to expose type-errors! RELATION tgt[Term*Concept] ENDPATTERN -- (Show demo: src and tgt remain empty, -- but source and target are filled) PROCESS "Defining type-terms" RELATION dom[Term*TypeTerm] [UNI] -- TOT is maintained in RULE "dom is total" RELATION cod[Term*TypeTerm] [UNI] -- TOT is maintained in RULE "cod is total" RELATION pop[Concept*TypeTerm] [UNI] -- TOT is maintained in RULE "pop is total" RELATION sub[TypeTerm*TypeTerm] RELATION subStar[TypeTerm*TypeTerm] RELATION subPlus[TypeTerm*TypeTerm] RELATION subCopy[TypeTerm*TypeTerm] RULE "Compute transitive closure of sub" : sub = subCopy VIOLATION (TXT "{EX}_; TransitiveClosure_;sub_;TypeTerm_;subCopy_;subPlus") ROLE ExecEngine MAINTAINS "Compute transitive closure of sub" -- "subPlus = sub+" (implicitly) RULE "Compute subStar from subPlus" : subStar = subPlus\/I VIOLATION (TXT "{EX}_; InsPair_;subStar_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS "Compute subStar from subPlus" RULE "dom is total" : I[Term] |- dom;dom~ VIOLATION (TXT "{EX}_; InsPair_;dom_;Term_;", SRC I, TXT "_;TypeTerm_;dom(", SRC I, TXT ")") ROLE ExecEngine MAINTAINS "dom is total" RULE "cod is total" : I[Term] |- cod;cod~ VIOLATION (TXT "{EX}_; InsPair_;cod_;Term_;", SRC I, TXT "_;TypeTerm_;cod(", SRC I, TXT ")") ROLE ExecEngine MAINTAINS "cod is total" RULE "pop is total" : I[Concept] |- pop;pop~ VIOLATION (TXT "{EX}_; InsPair_;pop_;Concept_;", SRC I, TXT "_;TypeTerm_;pop(", SRC I, TXT ")") ROLE ExecEngine MAINTAINS "pop is total" ENDPROCESS PROCESS "Define order on type-terms" {-Example: dom(r) |- pop(A) -} RULE insDomRelation : dom~;source;pop |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS insDomRelation RULE insCodRelation : cod~;target;pop |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS insCodRelation {-Example: dom(s;t) |- dom(s) -} RULE domainDomComposition : dom~;I[Composition];first;dom |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS domainDomComposition RULE domainCodComposition : cod~;I[Composition];second;cod |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS domainCodComposition {- Example s;t has a type-term between s and t -} RELATION inter[Composition*TypeTerm] RULE compositionNewTypeTerm : I[Composition] |- inter;inter~ VIOLATION (TXT "{EX}_; InsPair_;inter_;Composition_;", SRC I, TXT "_;TypeTerm_;inter(", SRC I, TXT ")" ,TXT "{EX}_; InsPair_;sub_;TypeTerm_;inter(", SRC I, TXT ")_;TypeTerm_;", SRC first;cod,TXT "{EX}_; InsPair_;sub_;TypeTerm_;inter(", SRC I, TXT ")_;TypeTerm_;", SRC second;dom ) ROLE ExecEngine MAINTAINS compositionNewTypeTerm RULE betweenCompositionFirst : inter~;first;cod |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS betweenCompositionFirst RULE betweenCompositionSecond : inter~;second;dom |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS betweenCompositionSecond RULE domainDomRule : dom~;lhsTerm~;rhsTerm;dom \/ dom~;rhsTerm~;lhsTerm;dom |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS domainDomRule RULE domainCodRule : cod~;lhsTerm~;rhsTerm;cod \/ cod~;rhsTerm~;lhsTerm;cod |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS domainCodRule ENDPROCESS PROCESS "Type assignment" RELATION pretype[TypeTerm*Concept] RULE "Insert into pretype" : subStar;pop~ |- pretype VIOLATION (TXT "{EX}_; InsPair_;pretype_;TypeTerm_;", SRC I, TXT "_;Concept_;", TGT I) ROLE ExecEngine MAINTAINS "Insert into pretype" RELATION isa[Concept*Concept] RULE "Insert into isa" : pop;subPlus;pop~ - I |- isa VIOLATION (TXT "{EX}_; InsPair_;isa_;Concept_;", SRC I, TXT "_;Concept_;", TGT I) ROLE ExecEngine MAINTAINS "Insert into pretype" RULE signatureInsDom : dom;(pretype - pretype;isa) |- src VIOLATION (TXT "{EX}_; InsPair_;src_;Term_;", SRC I, TXT "_;Concept_;", TGT I) ROLE ExecEngine MAINTAINS signatureInsDom RULE signatureInsCod : cod;(pretype - pretype;isa) |- tgt VIOLATION (TXT "{EX}_; InsPair_;tgt_;Term_;", SRC I, TXT "_;Concept_;", TGT I) ROLE ExecEngine MAINTAINS signatureInsCod ENDPROCESS PROCESS "Type checking" RULE "Unambiguous signature" : src;-I[Concept];src~ \/ tgt;-I[Concept];tgt~ |- -I[Term] MESSAGE "Every term should have a unique signature." VIOLATION (SRC I, TXT " has multiple signatures.") ROLE User MAINTAINS "Unambiguous signature" RULE "Complete pretype" : I[TypeTerm] |- pretype;pretype~ MESSAGE "Every type-term must have one concept as its pretype." VIOLATION (SRC I, TXT " has no pretype.") ROLE User MAINTAINS "Complete pretype" RULE compositionCheck : I[Composition];first;tgt |- (src~;second~)\I MESSAGE "Source and target in a composition must match." VIOLATION ( SRC I, TXT ": the tgt of " , SRC first, TXT " is " , TGT I, TXT " and " , SRC second;src, TXT " is the src of " , SRC second, TXT ", which is a mismatch." ) ROLE User MAINTAINS compositionCheck ENDPROCESS -- Wrap up: -- 1. Algorithm in Haskell in our paper. -- 2. Description in Relation Algebra presented -- in Ampersand. -- 3. Contribution: Visualization (in paper) -- 4. Contribution: types by domain analysis -- 5. Why we like it: it is simple! -- 6. Why we don't like it: it is too powerful, -- at the expense of confusing users. --PROCESS "Intersections" -- RULE domainCodIntersection : -- cod~;I[Intersection];first;cod -- \/ cod~;I[Intersection];second;cod |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS domainCodIntersection -- RULE domainDomIntersection : -- dom~;I[Intersection];first;dom -- \/ dom~;I[Intersection];second;dom |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) ROLE ExecEngine MAINTAINS domainDomIntersection --ENDPROCESS --PROCESS "Minuses" ROLE ExecEngine MAINTAINS domainDomMinus, domainCodMinus -- RULE domainDomMinus : -- dom~;I[Minus];first[BinaryTerm*Term];dom |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) -- RULE domainCodMinus : -- cod~;I[Minus];second[BinaryTerm*Term];cod |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) --ENDPROCESS --PROCESS "Converses" ROLE ExecEngine MAINTAINS converseDom, converseDomFlp, converseCod, converseCodFlp -- RULE converseDom : -- dom~;I[Converse];arg;cod |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) -- RULE converseDomFlp : -- dom~;I[Converse];arg;cod |- sub~ VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", TGT I, TXT "_;TypeTerm_;", SRC I) -- RULE converseCod : -- cod~;I[Converse];arg;dom |- sub VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", SRC I, TXT "_;TypeTerm_;", TGT I) -- RULE converseCodFlp : -- cod~;I[Converse];arg;dom |- sub~ VIOLATION (TXT "{EX}_; InsPair_;sub_;TypeTerm_;", TGT I, TXT "_;TypeTerm_;", SRC I) --ENDPROCESS PROCESS Atoms RELATION isa[Concept*Concept] [IRF,ASY] MEANING "s isa g means that each element of concept s is defined to be an element of concept g as well." RELATION isaStar[Concept*Concept] -- Transitive, reflexive closure of isa, aka isa* RELATION isaPlus[Concept*Concept] -- Transitive closure of isa, aka isa+ RELATION isaCopy[Concept*Concept] -- necessary only for calling the Transitive closure function. ROLE ExecEngine MAINTAINS "Compute transitive closure of isa" RULE "Compute transitive closure of isa" : isa = isaCopy VIOLATION (TXT "{EX} TransitiveClosure;isa;Concept;isaCopy;isaPlus") ROLE ExecEngine MAINTAINS "Compute transitive closure of isa by Ins", "Compute transitive closure of isa by Del" RULE "Compute transitive closure of isa by Ins" : isaPlus\/I |- isaStar VIOLATION (TXT "{EX} InsPair;isaStar;Concept;", SRC I, TXT ";Concept;", TGT I) RULE "Compute transitive closure of isa by Del" : isaStar |- isaPlus\/I VIOLATION (TXT "{EX} DelPair;isaStar;Concept;", SRC I, TXT ";Concept;", TGT I) ENDPROCESS INTERFACE "DomainAnaylsis" FOR User : '_SESSION' TABS[ relations : V[SESSION*Relation] BOX [ relation : I , source : source , target : target ] , rules : V[SESSION*Rule] ROWS [ rule : I , lhsTerm : lhsTerm , rhsTerm : rhsTerm ] , terms : V[SESSION*Term] BOX [ "term " : I , src : src , tgt : tgt ] , "type-terms" : V[SESSION*TypeTerm] BOX [ "type-term" : I , "sub+" : subPlus , pretype : pretype ] ] VIEW Term : Term(I) VIEW Rule : Rule(lhsTerm, TXT " = ", rhsTerm) VIEW Relation : Relation(I, TXT "[", source, TXT "*", target, TXT "]") ENDCONTEXT