# The Verse Calculus: a Core Calculus for Functional Logic Programming

DevFeed: [The Verse Calculus: a Core Calculus for Functional Logic Programming](<https://devfeed.tech/articles/the-verse-calculus-a-core-calculus-for-functional-logic-programming-29489.md>)

Original publisher: [Read original article](<http://lambda-the-ultimate.org/node/5662>)

Published: 2022-12-12T16:23:17Z

Content type: article

Language: en

Sources: [Lambda the Ultimate](<https://devfeed.tech/sources/lambda-the-ultimate.md>)

Topics: [Programming](<https://devfeed.tech/topics/programming.md>), [Math and Logic](<https://devfeed.tech/topics/math-and-logic.md>)

Tags: [draft](<https://devfeed.tech/tags/draft.md>), [functional](<https://devfeed.tech/tags/functional.md>), [lambda-calculus](<https://devfeed.tech/tags/lambda-calculus.md>), [languages](<https://devfeed.tech/tags/languages.md>), [logic](<https://devfeed.tech/tags/logic.md>), [paper](<https://devfeed.tech/tags/paper.md>), [programming](<https://devfeed.tech/tags/programming.md>), [rewrite](<https://devfeed.tech/tags/rewrite.md>), [semantics](<https://devfeed.tech/tags/semantics.md>)

## AI overview

The draft paper introduces the Verse calculus (VC), a core calculus for functional logic programming. Its main contribution is a small-step rewrite semantics that enables reasoning about VC programs through successive rewrites, as with lambda calculus. The authors note that the design is still a work in progress and that the current rewrite rules may not be confluent.

## Source excerpt

The Verse Calculus: a Core Calculus for Functional Logic Programming https://simon.peytonjones.org/assets/pdfs/verse-conf.pdf LENNART AUGUSTSSON, Epic Games, Sweden JOACHIM BREITNER KOEN CLAESSEN, Epic Games, Sweden RANJIT JHALA, Epic Games, USA SIMON PEYTON JONES, Epic Games, United Kingdom OLIN SHIVERS, Epic Games, USA/li> TIM SWEENEY, Epic Games, USA Functional logic languages have a rich literature, but it is tricky to give them a satisfying semantics. In this paper we describe the Verse calculus, VC, a new core calculus for functional logical programming. Our main contribution is to equip VC with a small-step rewrite semantics, so that we can reason about a VC program in the same way as one does with lambda calculus; that is, by applying successive rewrites to it. This draft paper describes our current thinking about Verse. It is very much a work in progress, not a finished product. The broad outlines of the design are stable. However, the details of the rewrite rules may well change; we think that the current rules are not confluent, in tiresome ways. (If you are knowledgeable about confluence proofs, please talk to us!)We are eager to enagage in a dialogue with the community. Please do write to us.