Skip to content

Instantly share code, notes, and snippets.

@stackdump

stackdump/tic-tac-toe-dependent-types.md

Last active June 13, 2024 13:41
Show Gist options
  • Save stackdump/2be8345c71ab111a6c37d97bdea84234 to your computer and use it in GitHub Desktop.
Save stackdump/2be8345c71ab111a6c37d97bdea84234 to your computer and use it in GitHub Desktop.
Download ZIP
Describing Tic-Tac-Toe Using Dependent Sum Types
Raw
tic-tac-toe-dependent-types.md

Problem

Can we use Type Theory to show that a given Petri-Net correctly models a game of Tic-Tac-Toe?

EDIT: removed a bad attempt to grapple with this problem originally in 2017

@stackdump
Copy link
Author

stackdump commented Dec 3, 2017 •
edited
Loading

EDIT: removed some thoughts about state space...

@stackdump
Copy link
Author

Also more interesting material here https://www.euclideanspace.com/maths/discrete/types/dependent/index.htm

It seems like we can claim that the vector representation in code is a dependent sum type.
Meets the rules:

It also has this commentary

In computer programs they provide a sort of 
meta level capability to types in that
terms can be used at compile time and not just runtime.

@stackdump
Copy link
Author

stackdump commented Jun 13, 2024 •
edited
Loading

https://partialflow.wordpress.com/2017/07/26/dependent-types-type-level-programming/

I should really try coding a petri-net in Idris or some theorem proving language

@stackdump
Copy link
Author

Some work from 2022 https://amr-sabry.luddy.indiana.edu/files/2022/01/popl22main-p31-p-32bd461e9d-54940-final.pdf

and more directly related to category theory

https://math.libretexts.org/Bookshelves/Applied_Mathematics/Seven_Sketches_in_Compositionality:_An_Invitation_to_Applied_Category_Theory_(Fong_and_Spivak)/06:_Circuits_-_Hypergraph_Categories_and_Operads/6.01:_The_ubiquity_of_network_languages

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment