Knowledge representation, computation, and learnin

KnowledgeRepresentation,Computation,andLearninginHigher-orderLogicJ.W.LloydComputerSciencesLaboratoryResearchSchoolofInformationSciencesandEngineeringAustralianNationalUniversityDRAFT,August1,2002AbstractThispapercontainsasystematicstudyofthefoundationsofknowledgerepresentation,computation,andlearninginhigher-orderlogic.First,apolymorphically-typedhigher-orderlogic,whoseoriginscanbetracedbacktoChurch'ssimpletheoryoftypes,ispresented.Amodeltheoryandprooftheoryforthislogicaredevelopedandbasictheoremsrelatingthesetwoaregiven.Ametricspaceofcertainclosedterms,whichprovidesarichlanguageforrepresentingindividuals,isthenstudied.Kernelfunctionsthatcanprovidethebasisofvariouslearningmethodsaredenedonthisspace.Alsoamethodofsystematicallyconstructingpredicatesonsuchindividualsisgiven.Thetechniqueofprogrammingwithabstractionsisillustrated.Majorapplicationsofthelogictodeclarativeprogramminglanguagesandmachinelearningareindicated.cJ.W.Lloyd,2002Contents1Introduction32TheLogic32.1Types...........................................32.2TypeSubstitutions....................................62.3Terms...........................................92.4TermSubstitutions....................................192.5Schemas..........................................282.6SchemaSubstitutions..................................312.7StatementsandStatementSchemas..........................332.8-conversion........................................352.9Axioms..........................................412.10ModelTheory.......................................422.11ProofTheory.......................................443RepresentationofIndividuals473.1DefaultTerms.......................................473.2NormalTerms.......................................513.3AnEquivalenceRelationonNormalTerms......................543.4ATotalOrderonNormalTerms............................563.5BasicTerms........................................583.6AMetriconBasicTerms................................643.7AKernelonBasicTerms................................703.8APartialOrderonBasicTerms.............................743.9SomeExamplesofRepresentation...........................763.10First-orderversusHigher-orderRepresentation....................794PredicateConstruction804.1Transformations.....................................814.2StandardPredicates...................................844.3RegularPredicates....................................874.4TheImplicationPreorder................................884.5TheRelation......................................924.6EnumeratingRegularPredicates............................934.7AnExampleofPredicateConstruction.........................955ProgrammingwithAbstractions985.1ListProcessing......................................995.2SetandMultisetProcessing...............................1006Conclusions1037Acknowledgements105References105ADenitionsofSomeBasicFunctions10731IntroductionThispapercontainsanaccountofapolymorphicallytyped,higher-orderlogicmainlyintendedforuseasabasisfordeclarativeprogramminglanguagesandlearningsystems.Historically,thislogiccanbetracedbacktoChurch'ssimpletheoryoftypes[Chu40],whichIrefertoastypetheoryinthefollowing.TheappropriatemodeltheoryfortypetheorywasgivensubsequentlybyHenkinin[Hen50].Morerecentaccountsoftypetheoryappearin[And86]and[Wol93].Accountsofintuitionisticversionsofthelogicarein[Bel88]and[LS86].Infact,thelogicpresentedhereextendstypetheoryinthatitispolymorphicandadmitsproducttypes.Thepolymorphismintroducedisasimpleformofparametricpolymorphism.Adeclarationforapolymorphicconstantisunderstoodasstandingforacollectionofdeclarationsforthe(monomorphic)constantswhichcanbeobtainedbyinstantiatingallparametersinthepolymorphicdeclarationwithclosedtypes.Similarly,apolymorphictermcanberegardedasstandingforacollectionof(monomorphic)terms.Furthermore,themodel-theoreticsemanticsofpolymorphictypetheorycaneasilybereducedtothatof(monomorphic)typetheorybyadoptingthisviewofthepolymorphism.AnotherdierencecomparedtotheoriginalformulationoftypetheoryisthattheprooftheorydevelopedbyChurch(andothers)ismodiedheretogiveamoredirectformofequationalreasoningthatisbettersuitedtotheapplicationofthelogicasafoundationfordeclarativeprogramminglanguages.Ametricspaceofclosedtermsthatissuitableforrepresentingindividualsindiverseapplica-tionsisidentied.Themostinterestingaspectofthisspaceoftermsisthatitincludescertainabstractionsandthereforeismuchwiderthanisnormallyconsideredforknowledgerepresentation.Theseabstractionsallowonetomodelsets,multisets,andsimilardatatypes,inanelegantway.Asystematicmethodofconstructingpredicatesonindividualsisstudied.Forthispurpose,particularkindsoffunctions,calledtransformations,aredenedandpredicatesareincrementallyconstructedbycomposingtransformations.Thisleadstoa,generallylarge,setofpredicatesthatmustbesearchedtondasuitablepredicatefortheapplicationathand.Basictheoreticalpropertiesofthissetofpredicatesareprovided.Thelogicissuitableasafoundationfordeclarativeprogramminglanguages,forexample,[Je],[He],and[Llo99].Thelogicalsoprovid