Alexander VargaNatural Tranformations

Created by Alexander Varga
 ``` 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79``` ``` # Solutions to https://forum.azimuthproject.org/discussion/2244/lecture-43-chapter-3-natural-transformations # Finds all natural transformations between 2 functors in 1 -> Set from z3 import * # Microsoft's Theorem Prover s = Solver() # Define F(People) = {Alice, Bob, Stan, Tyler} and F(Friend) F = {} F['People'], F['members'] = EnumSort('F(People)', ('Alice', 'Bob', 'Stan', 'Tyler')) F['Alice'], F['Bob'], F['Stan'], F['Tyler'] = F['members'] F['Friend'] = Function('F(Friend)', F['People'], F['People']) s.add(F['Friend'](F['Alice']) == F['Bob']) s.add(F['Friend'](F['Bob']) == F['Alice']) s.add(F['Friend'](F['Stan']) == F['Alice']) s.add(F['Friend'](F['Tyler']) == F['Stan']) F['x'] = Const('F(person)', F['People']) # Variable in F(People) # Define G(People) = {Alice, Bob, Stan, Tyler, Mei-Chu} and G(Friend) G = {} G['People'], G['members'] = EnumSort('G(People)', ('Alice', 'Bob', 'Stan', 'Tyler', 'Mei-Chu')) G['Alice'], G['Bob'], G['Stan'], G['Tyler'], G['Mei-Chu'] = G['members'] G['Friend'] = Function('G(Friend)', G['People'], G['People']) s.add(G['Friend'](G['Alice']) == G['Bob']) s.add(G['Friend'](G['Bob']) == G['Alice']) s.add(G['Friend'](G['Stan']) == G['Alice']) s.add(G['Friend'](G['Tyler']) == G['Stan']) s.add(G['Friend'](G['Mei-Chu']) == G['Stan']) G['x'] = Const('G(person)', G['People']) # Variable in G(People) # Define H(People) = {Alice, Bob, Tyler} and H(Friend) H = {} H['People'], H['members'] = EnumSort('H(People)', ('Alice', 'Bob', 'Tyler')) H['Alice'], H['Bob'], H['Tyler'] = H['members'] H['Friend'] = Function('H(Friend)', H['People'], H['People']) s.add(H['Friend'](H['Alice']) == H['Bob']) s.add(H['Friend'](H['Bob']) == H['Alice']) s.add(H['Friend'](H['Tyler']) == H['Bob']) H['x'] = Const('H(person)', H['People']) # Variable in H(People) # Choose source and target functors of natural transformation a S, T = F, G # Define commutativity constraints on a_Friend a = {} a['Friend'] = Function('a_Friend', S['People'], T['People']) s.add(ForAll(S['x'], T['Friend'](a['Friend'](S['x'])) == a['Friend'](S['Friend'](S['x'])))) # Print all satisfying models while s.check() == sat: m = s.model() print(", ".join("{} -> {}".format(person, m.evaluate(a['Friend'](person))) for person in S['members'])) s.add(Exists(S['x'], a['Friend'](S['x']) != m.evaluate(a['Friend'](S['x'])))) ### F -> G ### # Alice -> Alice, Bob -> Bob, Stan -> Stan, Tyler -> Tyler # Alice -> Bob, Bob -> Alice, Stan -> Alice, Tyler -> Stan # Alice -> Alice, Bob -> Bob, Stan -> Stan, Tyler -> Mei-Chu # Alice -> Alice, Bob -> Bob, Stan -> Bob, Tyler -> Alice # Alice -> Bob, Bob -> Alice, Stan -> Alice, Tyler -> Bob ### F -> H ### # Alice -> Alice, Bob -> Bob, Stan -> Bob, Tyler -> Alice # Alice -> Bob, Bob -> Alice, Stan -> Alice, Tyler -> Bob # Alice -> Alice, Bob -> Bob, Stan -> Bob, Tyler -> Tyler ### H -> H ### # Alice -> Alice, Bob -> Bob, Tyler -> Tyler # Alice -> Alice, Bob -> Bob, Tyler -> Alice # Alice -> Bob, Bob -> Alice, Tyler -> Bob ```