Automated bijections with combinatorial exploration

Abstract

Bijections appear in most areas of mathematics. They are of particular importance in the field of combinatorics, where they are a way of enumerating families of objects. The aim of this thesis was to develop a fully automated and domain agnostic bijection search built on top of an existing automated combinatorial specification framework. We definea binary relation on specifications that structurally associates them. When satisfied, a bijection can be constructed between their classes. This theoretical foundation is accompanied by a search algorithm for specifications satisfying this relation. The algorithm utilizes dynamic programming and backtracking. If a bijection is found it can map objects between the classes of the specifications, in both directions. Thesearch algorithm was mainly applied to the domain of permutation patterns, where a total of 189 bijections were discovered, excluding symmetries and compositions. In many cases no previous bijections were known. Some cross-domain bijections were also discovered. As far as we know, this is the first ever fully automated bijection framework, with prior attempts requiring preliminary mathematical work. This workoffers substantial structural insight into classes and can be considered a significant innovation in automated mathematics.

Gagntækar varpanir koma við sögu á flestum sviðum stærðfræðinnar. Þær eru sérstaklega mikilvægar innan fléttufræði þar sem þær geta talið fjölskyldur hluta. Markmið þessa verkefnis var að þróa leit að gagntækum vörpunum sem er óháð þeim hlutum sem unnið er með, að öllu leyti sjálfvirk og byggð á kerfi sjálfvirkra fléttufræðilegra forskrifta. Við skilgreinum tvístæð vensl á forskriftir sem vensla þær út frá uppbyggingu sem nota má til að mynda gagntæka vörpun þeirra á milli. Þessum fræðilega grunni fylgir leitarreiknirit sem leitar að vensluðum forskriftum. Reikniritið notast við kvika bestun og hopun. Ef gagntæk vörpun finnst þá má varpa stökum flokka forskriftanna í báðar áttir. Leitinni var einkum beitt á umraðanamynstur, þar sem 189 gagntækar varpanir fundust, að undanskildum samhverfum og samskeytingum. Ímörgum tilfellum voru engar gagntækar varpanir þekktar áður. Einnig voru nokkrar gagntækar varpanir uppgötvaðar milli ólíkra hluta. Eftir því sem best er vitað er þetta fyrsta kerfi sem finnur og myndar gagntækar varpanir sem er að öllu leyti sjálfvirkt en fyrri kerfi kröfðust stærðfræðilegs undirbúnings. Þessi vinna gefur mikla innsýn íuppbyggingu flokka og er þýðingarmikil nýjung í heimi sjálfvirkrar stærðfræði.