[msp-interest] [MSP101] Conor McBride: Wiggle It Just a Little Bit (1pm Mon 19/1, LT210)

[Fiona Blackett]

Hello all,

We're gonna be kicking off our MSP101 this semester with a talk from Conor McBride on Monday! Hope to see you there.

Cheers,
Fiona Blackett
----------------------------------------------------------------------------------------------

Date, time and place:
 Monday 19th January, 1:00 pm, Livingstone Tower room LT210

Speaker:
 Conor McBride (MSP)

Title:
  Wiggle It (Just a Little Bit)

Zoom Link:
 https://strath.zoom.us/j/82143788147?pwd=dMy8sftupiQ8eEiIqLzodkMra6RTfn.1
Meeting ID: 821 4378 8147
Password: whiteboard

Abstract:
  Testing can reveal the absence of bugs in situations where we can show that the test data expose all the possible variations. This is straightforward when the domain is finite, but one can also achieve test coverage for large domains by restricting the ways in which the program may process its input. For example, the fact that the sum of the numbers less than n is n choose 2 can be proven by testing for n in {0, 1, 2} because both calculations are inherently quadratic. I have, on and off, been thinking about how to deliver similar results for other inductive data structures. For example, one can generate particularly well behaved folds on unlabelled binary trees by giving (i) the tree which is the image of the leaf, and (ii) a tree with two variables showing how the ouptut for a node is computed from the outputs for its two subtrees. I claim that if two such folds agree at the four smallest trees, then they agree for all trees. Clearly, we recover (i) by testing at a leaf. We recover (ii) by testing at a node with leaves for subtrees, then perturbing each of those subtrees in turn, to see where the output changes. That is to say, we use perturbation to recover abstraction. I am currently working on a proof of this claim in Agda and will share my progress (and my prospectus) in this talk.
----------------------------------------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20260116/0031e1e3/attachment.html