Abductive functional programming, a semantic approach

TL;DR

This paper introduces a call-by-value lambda calculus with an abductive inference-inspired construct, providing a semantic framework and proving soundness and termination properties, with a visual implementation.

Contribution

It presents a novel abductive construct in lambda calculus, along with a semantic model based on Geometry of Interaction, and proves its soundness and termination.

Findings

The calculus is sound and well-typed programs terminate normally.

A visual implementation of the semantics is provided.

Soundness is proven for both the core calculus and the garbage collection rules.

Abstract

We propose a call-by-value lambda calculus extended with a new construct inspired by abductive inference and motivated by the programming idioms of machine learning. Although syntactically simple the abductive construct has a complex and subtle operational semantics which we express using a style based on the Geometry of Interaction. We show that the calculus is sound, in the sense that well typed programs terminate normally. We also give a visual implementation of the semantics which relies on additional garbage collection rules, which we also prove sound.