Nierozstrzygalność semiunifikacji na chuseczce do nosa

Problem semiunifikacji pojawia się naturalnie w zagadnieniach związanych z typowalnością programów funkcyjnych, w których systemy typów opartych na systemie F. Intuicyjnie chodzi tutaj o typowanie, w którym funkcji w programie staramy się przypisać jak najbardziej ogólny typ, a potem w miejscu użycia pozwalamy, aby ten typ został uszczegółowiony zgodnie z konkretnymi potrzebami. Niedawno Andrej Dudenhefner opublikował bardzo zgrabny i krótki dowód nierozstrzygalności problemu seminunifikacji. Zostanie przedstawiony właśnie ten dowód.