interdisciplinary computing (domcode)

Transcript

1. interdisciplinary computing ~ theory and practice
2. @igorwhilefalse
3. #HackTheStigma ✊
4. interdisciplinary thinking
5. knitting ~ theorem proving
6. grammars ~ linguistics
7. finance ~ information theory
8. information theory ~ statistics
9. algorithms ~ feminism
10. code complexity ~ applied psychology
11. computation ~ formal logic
12. formal logic ~ electronics
13. electronics ~ physics
14. physics ~ information theory
15. computation ~ cosmic rays
16. Chapter I ≈ Theory
17. weaving programs
19. @sydneypadua
23. from maths to logic
27. from logic to electronics
31. • 1600: leibniz devises binary numbers • 1800: boole + de morgan supply the laws • 1937: 1-bit binary adder • 1947: transistors • 1947: error correcting codes • 1948: information theory • 1965: cosmic radiowave background • 1969: unix • 1972: c programming language
32. • 1600: leibniz devises binary numbers • 1800: boole + de morgan supply the laws • 1937: 1-bit binary adder • 1947: transistors • 1947: error correcting codes • 1948: information theory • 1965: cosmic radiowave background • 1969: unix • 1972: c programming language
33. • 1600: leibniz devises binary numbers • 1800: boole + de morgan supply the laws • 1937: 1-bit binary adder • 1947: transistors • 1947: error correcting codes • 1948: information theory • 1965: cosmic radiowave background • 1969: unix • 1972: c programming language
34. self-reference and something something quines
37. data = %q{ program = "data = %q{#{data}}" + data puts program } program = "data = %q{#{data}}" + data puts program
40. artsnfood.blogspot.com
41. Chapter II ≈ Practice
42. logic programming
43. miniKanren
44. µKanren (define (var c) (vector c)) (define (var? x) (vector? x)) (define (var=? x1 x2) (= (vector-ref x1 0) (vector-ref x2 0))) (define (walk u s) (let ((pr (and (var? u) (assp (lambda (v) (var=? u v)) s)))) (if pr (walk (cdr pr) s) u))) (define (ext-s x v s) `((,x . ,v) . ,s)) (define (== u v) (lambda (s/c) (let ((s (unify u v (car s/c)))) (if s (unit `(,s . ,(cdr s/c))) mzero)))) (define (unit s/c) (cons s/c mzero)) (define mzero '()) (define (unify u v s) (let ((u (walk u s)) (v (walk v s))) (cond ((and (var? u) (var? v) (var=? u v)) s) ((var? u) (ext-s u v s)) ((var? v) (ext-s v u s)) ((and (pair? u) (pair? v)) (let ((s (unify (car u) (car v) s))) (and s (unify (cdr u) (cdr v) s)))) (else (and (eqv? u v) s))))) (define (call/fresh f) (lambda (s/c) (let ((c (cdr s/c))) ((f (var c)) `(,(car s/c) . ,(+ c 1)))))) (define (disj g1 g2) (lambda (s/c) (mplus (g1 s/c) (g2 s/c)))) (define (conj g1 g2) (lambda (s/c) (bind (g1 s/c) g2))) (define (mplus $1 $2) (cond ((null? $1) $2) ((procedure? $1) (lambda () (mplus $2 ($1)))) (else (cons (car $1) (mplus (cdr $1) $2))))) (define (bind $ g) (cond ((null? $) mzero) ((procedure? $) (lambda () (bind ($) g))) (else (mplus (g (car $)) (bind (cdr $) g)))))
45. • ∧ conjunction • ∨ disjunction • = unification • ∃ variables
46. (run 1 (q) (== q 'hello)) ;=> (hello)
47. (run 1 (q) (== #t #f)) ;=> ()
48. (run 1 (q) (== q 'doughnut) (== q 'bagel)) ;=> ()
49. (run* (q) (conde [(== q 'doughnut)] [(== q 'bagel)])) ;=> (doughnut bagel)
50. theorem proving
51. (run* (q) (conde [(== q 'doughnut)] [(== q 'bagel)])) ∃q(doughnut(q) ∨ bagel(q))
52. ∃q(doughnut(q) ∨ bagel(q)) doughnut(q) ∨ bagel(q) ------------------- doughnut(q) ∨&e1
53. ∃q(doughnut(q) ∨ bagel(q)) doughnut(q) ∨ bagel(q) ------------------- bagel(q) ∨&e2
54. the never ending search for answers
55. (define nevero (conde [(== #t #f)] [nevero])) (run 1 (q) nevero)
56. run (run 1 (q) nevero)
57. run nevero (run 1 (q) nevero)
58. run nevero (define nevero (conde [(== #t #f)] [nevero]))
59. run nevero (== #t #f) (define nevero (conde [(== #t #f)] [nevero]))
60. run nevero (== #t #f) X (define nevero (conde [(== #t #f)] [nevero]))
61. run nevero (== #t #f) X nevero (define nevero (conde [(== #t #f)] [nevero]))
62. run nevero (== #t #f) X nevero (define nevero (conde [(== #t #f)] [nevero]))
63. (== #t #f) run nevero (== #t #f) X nevero (define nevero (conde [(== #t #f)] [nevero]))
64. (== #t #f) run nevero (== #t #f) X nevero X (define nevero (conde [(== #t #f)] [nevero]))
65. (== #t #f) run nevero (== #t #f) X nevero X ... (define nevero (conde [(== #t #f)] [nevero]))
66. entscheidungsproblem
67. simulating concrete machines
69. AND OR
70. AND OR NOR
71. XNOR NAND
72. XOR XOR AND OR NOR
74. (define bit-xoro (lambda (x y r) (conde ((== 0 x) (== 0 y) (== 0 r)) ((== 1 x) (== 0 y) (== 1 r)) ((== 0 x) (== 1 y) (== 1 r)) ((== 1 x) (== 1 y) (== 0 r))))) (define bit-ando (lambda (x y r) (conde ((== 0 x) (== 0 y) (== 0 r)) ((== 1 x) (== 0 y) (== 0 r)) ((== 0 x) (== 1 y) (== 0 r)) ((== 1 x) (== 1 y) (== 1 r)))))
75. (define half-addero (lambda (x y r c) (all (bit-xoro x y r) (bit-ando x y c))))
76. (define full-addero (lambda (b x y r c) (fresh (w xy wz) (half-addero x y w xy) (half-addero w b r wz) (bit-xoro xy wz c))))
77. (define +o (lambda (n m k) (addero 0 n m k))) (define -o (lambda (n m k) (+o m k n)))
78. (run* (x y) (+o x y '(1 0 1))) ;=> (((1 0 1) ()) ; (() (1 0 1)) ; ((1) (0 0 1)) ; ((0 0 1) (1)) ; ((1 1) (0 1)) ; ((0 1) (1 1)))
79. parsing grammars?!
80. flickr.com/photos/strangeloop2015/21793631118
82. exp := var | abs | app abs := "λ" var "." exp app := "(" exp " " exp ")"
83. exp := var | abs | app abs := "λ" var "." exp app := "(" exp " " exp ")" x λx.x λx.x x (λx.x) (λx.x) ...
84. (define exp (lambda (e) (conde [(symbolo e)] [(fresh (v e2) (symbolo v) (exp e2) (== e `(λ ,v . ,e2)))] [(fresh (e1 e2) (exp e1) (exp e2) (== e `(,e1 ,e2)))])))
85. (run 10 (q) (exp q)) ;=> (x ; (λ x . x) ; (x x) ; ...)
86. society6.com/product/binary-search-tree--comp-sci-series_print
87. flickr.com/photos/drjason/280369547
88. quines
89. making use of the church-turing thesis
91. (define eval-expo (lambda (exp env val) (conde ((fresh (v) (== `(quote ,v) exp) (not-in-envo 'quote env) (noo 'closure v) (== v val))) ((fresh (a*) (== `(list . ,a*) exp) (not-in-envo 'list env) (noo 'closure a*) (proper-listo a* env val))) ((symbolo exp) (lookupo exp env val)) ((fresh (rator rand x body env^ a) (== `(,rator ,rand) exp) (eval-expo rator env `(closure ,x ,body ,env^)) (eval-expo rand env a) (eval-expo body `((,x . ,a) . ,env^) val))) ((fresh (x body) (== `(lambda (,x) ,body) exp) (symbolo x) (not-in-envo 'lambda env) (== `(closure ,x ,body ,env) val)))))) (define not-in-envo (lambda (x env) (conde ((fresh (y v rest) (== `((,y . ,v) . ,rest) env) (=/= y x) (not-in-envo x rest))) ((== '() env))))) (define proper-listo (lambda (exp env val) (conde ((== '() exp) (== '() val)) ((fresh (a d t-a t-d) (== `(,a . ,d) exp) (== `(,t-a . ,t-d) val) (eval-expo a env t-a) (proper-listo d env t-d)))))) (define lookupo (lambda (x env t) (fresh (rest y v) (== `((,y . ,v) . ,rest) env) (conde ((== y x) (== v t)) ((=/= y x) (lookupo x rest t)))))) github.com/webyrd/quines
92. (run 1 (q) (eval-expo '((lambda (x) x) 'me!) '() q)) ;=> (me!)
93. (run 3 (q) (eval-expo q '() 'me!)) ;=> ('me! ; ((lambda (_.0) 'me!) '_.1) ; ((lambda (_.0) _.0) 'me!))
94. (run 1 (q) (eval-expo q '() q)) ;=> ((lambda (_.0) (list _.0 (list 'quote _.0))) ; '(lambda (_.0) (list _.0 (list 'quote _.0))))
96. conclusion
97. • ∧ conjunction (implicit) • ∨ disjunction (conde) • = unification (==) • ∃ variables (fresh)
98. artsnfood.blogspot.com
99. (21) The Reasoned Schemer
 Daniel Friedman, William Byrd, Oleg Kiselyov (22) Quine Generation via Relational Interpreters
 William Byrd, Eric Holk, Daniel Friedman (23) µKanren
 Jason Hemann, Daniel Friedman (4) How to Replace Failure by a List of Successes
 Philip Wadler (7) Unspeakable Things
 Laurie Penny
100. Thanks! Questions? •minikanren.org •gif.industries •@igorwhilefalse
101. References
102. (1) Knitting for Fun: A Recursive Sweater
 Anna Bernasconi, Chiara Bodei, Linda Pagli (2) Weaving and Programming: More Related Than You (Probably) Realize!
 Allie Jones (3) From Text to Textiles!
 Lea Albaugh (4) How to Replace Failure by a List of Successes
 Philip Wadler (5) A Mathematical Theory of Communication
 Claude Shannon
103. (6) Harassed by Algorithms
 Joanne McNeil (7) Unspeakable Things
 Laurie Penny (8) Cognitive Psychology and Programming Language Design
 Ben Shneiderman (9) Gödel, Escher, Bach
 Douglas Hofstadter (10) The Annotated Turing
 Charles Petzold
104. (11) Clause and Effect
 William Clocksin (12) Code
 Charles Petzold (13) Bitsquatting
 Artem Dinaburg (14) Redis Crashes - a small rant about software reliability
 Salvatore Sanfilippo (15) The Thrilling Adventures of Lovelace and Babbage
 Sydney Padua
105. (16) Logicomix: An Epic Search for Truth
 Apostolos Doxiadis, Christos Papadimitriou (17) Pioneer Programmer
 Jean Jennings Bartik (18) The C Programming Language
 Brian Kernighan, Dennis Ritchie (19) Understanding Computation
 Tom Stuart (20) Quantum Electrodynamics
 Richard Feynman
106. (21) The Reasoned Schemer
 Daniel Friedman, William Byrd, Oleg Kiselyov (22) Quine Generation via Relational Interpreters
 William Byrd, Eric Holk, Daniel Friedman (23) µKanren
 Jason Hemann, Daniel Friedman (24) Propositions as Types
 Philip Wadler (25) Unflattening
 Nick Sousanis