Snippets

Alexander Varga Natural Tranformations

Created by Alexander Varga

# 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)