Domain-Theoretic Semantics for Functional Logic Programming
summary
Reconstructs a typed FLP core calculus as call-by-push-value with algebraic effects, implements an abstract machine that performs weak head narrowing using logical-variable contexts, most-general unifiers and configuration trees, and models computations with the lower powerdomain to support countable nondeterminism. Proves the denotation is sound, adequate and fully abstract for the machine but also shows the model is termination-insensitive (failure and divergence collapse) and argues under reasonable equations that distinguishing them in a domain-theoretic model is essentially impossible.
AI-written summary · about
chapters (26)
- 0:00Introduction
- 0:22Functional logic programming
- 1:25FLP semantics history
- 2:08Core calculus with effects
- 3:10Types and value distinctions
- 4:12Core calculus laws
- 5:15Abstract machine design
- 6:20Effect-free transitions
- 7:03Handling nondeterminism
- 8:06Unification via MGU
- 9:08Weak head narrowing
- 9:51Program execution example
- 10:35Completeness for first-order
- 10:58Denotational semantics
- 11:39Nondeterminism and power domains
- 12:20Lower power domain
- 13:23Angelic vs demonic
- 14:04Scott-closed subsets
- 14:45Term denotation and failure
- 15:06Results and approximation
- 15:48Termination insensitivity
- 16:49Adequacy and relations
- 17:29Failure modeling challenges
- 18:12Failure vs divergence
- 19:36Summary and open questions
- 19:57Q&A