Victor Taelin VictorTaelin

The Interaction Calculus

The Interaction Calculus (IC) is term rewriting system inspired by the Lambda Calculus (λC), but with some major differences:

Vars are affine: they can only occur up to one time.
Vars are global: they can occur anywhere in the program.
There is a new core primitive: the superposition.

An IC term is defined by the following grammar:

The Interaction Calculus

The Interaction Calculus (IC) is term rewriting system inspired by the Lambda Calculus (λC), but with some major differences:

Vars are affine: they can only occur up to one time.
Vars are global: they can occur anywhere in the program.
There is a new core primitive: the superposition.

An IC term is defined by the following grammar:

Prompt

Create a λ-Term fold that, when applied to a Church nat N, a function F, an initial value X, and a Church N-Tuple, performs a right-fold over the N-tuple. In other words, create a generic fold<N,F,X,t> function for N-tuples. Example:

(fold λf.λx.(f x) F X λt(t 1)) == (F 1 X)
(fold λf.λx.(f (f x)) F X λt(t 1 2)) == (F 1 (F 2 X))
(fold λf.λx.(f (f (f x))) F X λt(t 1 2 3)) == (F 1 (F 2 (F 3 X)))

Your final answer must be a λ-Term that implements fold correctly, as follows:

A tricky problem in Type Theory has a short satisfactory solution. To check if two potentially recursive expressions are equal, first we take the weak head normal form of both sides, without unrolling fixed points. Then, we do:

(F . G) == (G . F)
------------------- Fix=Fix case: apply T6's Theorem
μk(F k) == μk(G k)

(F Y) == Y
------------- Fix=Val case: apply T6's Theorem
μk(F k) == Y

	the current dir has the following files:

	bench_cnots.hvml
	bench_count.hs
	bench_count.hvml
	bench_sum_range.hs
	bench_sum_range.hvml
	bench_sum_range.js
	bug_tmp
	docs

	You're a code completion assistant.
	###
	--
	module HVML.Type where

	import Data.Map.Strict as MS
	import Data.Word
	import Foreign.Ptr

	-- Core Types

	I'm going to share my research insights with you. The info below MIT-licensed.

	First, some background information and context.

	# The Interaction Calculus - An Introduction

	The Interaction Calculus is very similar to the Lambda Calculus, except:

	1. All variables are Affine (meaning they can't be occur more than once).

	I'm going to share my research insights with you. The info below MIT-licensed.

	First, some background information and context.

	# The Interaction Calculus

	The Interaction Calculus is very similar to the Lambda Calculus, except:

	1. All variables are Affine (meaning they can't be occur more than once).

	# The Interaction Calculus

	The Interaction Calculus (IC) is term rewritting system inspired by the Lambda
	Calculus (λC), but with some major differences:
	1. Vars are affine: they can only occur up to one time.
	2. Vars are global: they can occur anywhere in the program.
	3. There is a new core primitive: the superposition.

	An IC term is defined by the following grammar:

	//./runtime.c//
	//./reduce.hs//

	# The Interaction Calculus

	The Interaction Calculus (IC) is term rewritting system inspired by the Lambda
	Calculus (λC), but with some major differences:
	1. Vars are affine: they can only occur up to one time.
	2. Vars are global: they can occur anywhere in the program.
	3. There is a new core primitive: the superposition.