Page 1

A Proof of the Chip Model Separation Property in Alfa

Page 2

Bottom Line

Page 3

What Chip Model?

Page 4

Simplification

No failing algorithms

Page 5

Improved code reuse

One shared abstraction for finite maps

Page 6

Modularity / Abstracting away from irrelevant details

Page 7

Abstraction mechanisms

Page 8

Parameterizing over finite maps

First attempt

Page 9
Parameterizing over finite maps

Second attempt

Page 10

Assumed properties of finite maps

Page 11

Representation of algorithms

My definition of Alg:

Page 12

Assumed properties of algorithms

Page 13

Other required properties

Page 14

Types

Page 15

Formulation of the Channel Separation property

Consider two circuits:

Page 16
Formulation of the Channel Separation property

These two circuits produce the same output, provided

Page 17

Proof of the Channel Separation property

Page 18

Outline of the proof

Page 19

Alfa Files

Page 20

Conclusion

Page 21

The end

Questions?