Dynamic GoI machine

Dynamic GoI machine

Call-by-need and call-by-value graph rewriter

S-REPLS 4 (London), 27 September 2016

Koko Muroya & Dan Ghica (Univ. Birmingham)

Muroya (U. Birmingham)

• abstract machine to interpret λ-calculus

• a λ-term → a graph → moves of a token

GoI machine

2

compositionally

• Geometry of Interaction [Girard, ’89]

• “an execution path on a proof net”

Muroya (U. Birmingham)

GoI machine

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

q

q 1 1

Muroya (U. Birmingham)

GoI machine

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

q

q 1 1

Muroya (U. Birmingham)

call-by-name

• a token on a static graph

• space efficiency

• compositionality / interaction between components

• categorical GoI [Abramsky+, ’02]

• compilation to digital circuits [Ghica+, ’07-]

GoI machine

4

Muroya (U. Birmingham)

call-by-name call-by-value

• a token on a static graph

• space efficiency

GoI machine

5

CPS transformation (Schöpp, Hoshino+)

memory assigned to nodes (Hoshino+, Dal Lago+)

parallelism: multiple tokens (Dal Lago+)

dynamic jumps (Fernández+)

Muroya (U. Birmingham)

call-by-name call-by-value

• a token on a static graph

• dynamic rewrites & “checkpoint” mechanism

• space time efficiency

• compositional reasoning

• categorical GoI [Abramsky+, ’02]

Dynamic GoI machine

6

avoid repeated evaluation

force evaluation of function arguments

Muroya (U. Birmingham)

Avoid re-evaluation

7

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

q

q 3 q 3 6

Muroya (U. Birmingham)

Avoid re-evaluation

7

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

q

q 3 q 3 6

Muroya (U. Birmingham) 8

Avoid re-evaluation: dynamic rewrite

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham) 8

Avoid re-evaluation: dynamic rewrite

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham) 8

Avoid re-evaluation: dynamic rewrite

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

9

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

9

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

9

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

10

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

10

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

11

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

11

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

11

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

12

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

12

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

13

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

13

↵ : ! : : Cut : : C+ :

: p ↵ : ! : : Cut :

: p

? ? ! C

Cut

~ C

· · ·

↵

1

↵

m

↵ "

· · ·

· · ·

G

· · ·

· · ·

? ? !

Cut

↵

↵

↵

"

G

· · ·

· · ·

? ? ! C

Cut

~ C

· · ·

µ

µ

µ

⌫

1

· · ·

G ˜

· · ·

· · ·

1 m

⌫

⌫

Figure 5: Rewrite Transitions with Eliminating and Copying

A Materials for CRECOGI talk

Examples:

( x. x) 1

( x. x + x) (1 + 2) ( x. 0) (1 + 2)

Configures:

hM, Ei^t ‡ hE, A[V ]i^c ‡ hA[V ]i^a ‡ Call-by-need storeless abstract machine:

hV, Ei^t !^need hE, V i^c

hM N, Ei^t !^need hM, E[[ ] N ]i^t

hM + N, Ei^t !^need hM, E[[ ] + N ]i^t

hx, E₁[let x = N in E₂]i^t !^need hN, E₁[let x := [ ] in E₂[x]]]i^t h[ ], A[V ]i^c !^need hA[V ]i^a

hE[[ ] N ], A[ x. M ]i^c !^need hM [x⁰/x], E[A[let x⁰ = N in [ ]]]i^t hE[[ ] + N ], A[n]i^c !^need hN, E[A[n + [ ]]]i^t

hE[n + [ ]], A[m]i^c !^need hE, A[n + m]i^c

hE[let x = N in [ ]], A[V ]i^c !^need hE, let x = N in A[V ]i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[let x = V in E⁰]], V i^c

hE[let x := [ ] in E⁰[x]], A[V ]i^c !^need hE[A[E⁰]], V i^c (if x does not appear in E⁰)

6