{"action":"closed","issue":{"url":"https://api.github.com/repos/szymtor/locfin/issues/2","labels_url":"https://api.github.com/repos/szymtor/locfin/issues/2/labels{/name}","comments_url":"https://api.github.com/repos/szymtor/locfin/issues/2/comments","events_url":"https://api.github.com/repos/szymtor/locfin/issues/2/events","html_url":"https://github.com/szymtor/locfin/issues/2","id":53060788,"number":2,"title":"Zgniatanie templatów","user":{"login":"bklin","id":10338429,"avatar_url":"https://avatars.githubusercontent.com/u/10338429?v=3","gravatar_id":"","url":"https://api.github.com/users/bklin","html_url":"https://github.com/bklin","followers_url":"https://api.github.com/users/bklin/followers","following_url":"https://api.github.com/users/bklin/following{/other_user}","gists_url":"https://api.github.com/users/bklin/gists{/gist_id}","starred_url":"https://api.github.com/users/bklin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bklin/subscriptions","organizations_url":"https://api.github.com/users/bklin/orgs","repos_url":"https://api.github.com/users/bklin/repos","events_url":"https://api.github.com/users/bklin/events{/privacy}","received_events_url":"https://api.github.com/users/bklin/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":9,"created_at":"2014-12-29T18:39:48Z","updated_at":"2015-01-01T22:19:26Z","closed_at":"2015-01-01T22:19:26Z","body":"Suchejcie,\r\n\r\nChyba w końcu zapisałem (na licznych kartkach) dowód rzeczy następującej:\r\n\r\nDla dowolnego orbitowo-i-lokalnie skończonego templatu T istnieją\r\n   (i) skończony template T0\r\n   (ii) obliczalna w czasie wielomianowym procedura tłumaczenia (skończonych) instancji I nad T na instancje I0 nad T0,\r\ntakie że:\r\n   (A) dla każdej I, I ma rozwiązanie w T wtw. I0 ma rozwiązanie w T0,\r\n   (B) jeśli T ma polimorfizm rodzaju X to T0 też ma polimorfizm rodzaju X.\r\n\r\n(Z tym \"rodzajem X\" nie jestem jeszcze pewien co dokładnie pokazałem, ale to wyjdzie w praniu. W każdym razie majority/Malcev na T implikuje majority/Malcev na T0.)\r\n\r\nZauważcie że (B) to tylko jedna implikacja mojej wcześniejszej hipotezy H2. Nie mam pojęcia czy druga implikacja zachodzi, chyba nie. Ale może ta implikacja jest ważniejsza, bo ona niejako pokazuje że template T0 nie jest trudniejszy od T, a z kolei punkt (A) pokazuje że T nie jest trudniejszy od T0, co prawda tylko względem redukcji w czasie wielomianowym, ale lepszy rydz niż nic.\r\n\r\nW dowodzie (B) korzystam z Erykerii: jeśli T ma polimorfizm rodzaju X to ma też order-invariant polimorfizm rodzaju X. To chyba trochę ogranicza rodzaje X, co nie?\r\n\r\nZacznę to wpisywać do LaTeXa, ale pewnie skończę dopiero jutro.\r\n\r\n--Bartek"}}