Snippets

Alexander Varga Natural Tranformations

Created by Alexander Varga
snippet.BUILD
Raw 
 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

Comments (0)

HTTPS SSH

You can clone a snippet to your computer for local editing. Learn more.