• 検索結果がありません。

Dynamic GoI machine

N/A
N/A
Protected

Academic year: 2022

シェア "Dynamic GoI machine"

Copied!
57
0
0

読み込み中.... (全文を見る)

全文

(1)

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)

(2)

Muroya (U. Birmingham)

abstract machine to interpret λ-calculus

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

GoI machine

[Danos & Regnier ’99] [Mackie ’95]

2

compositionally

Geometry of Interaction [Girard, ’89]

“an execution path on a proof net”

(3)

Muroya (U. Birmingham)

GoI machine

[Danos & Regnier ’99] [Mackie ’95]

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

q

q 1 1

(4)

Muroya (U. Birmingham)

GoI machine

[Danos & Regnier ’99] [Mackie ’95]

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

q

q 1 1

(5)

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

[Danos & Regnier ’99] [Mackie ’95]

4

(6)

Muroya (U. Birmingham)

call-by-name call-by-value

a token on a static graph

space efficiency

GoI machine

[Danos & Regnier ’99] [Mackie ’95]

5

CPS transformation (Schöpp, Hoshino+)

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

parallelism: multiple tokens (Dal Lago+)

dynamic jumps (Fernández+)

(7)

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

(8)

Muroya (U. Birmingham)

Avoid re-evaluation

7

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

q

q 3 q 3 6

(9)

Muroya (U. Birmingham)

Avoid re-evaluation

7

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

q

q 3 q 3 6

(10)

Muroya (U. Birmingham) 8

Avoid re-evaluation: dynamic rewrite

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(11)

Muroya (U. Birmingham) 8

Avoid re-evaluation: dynamic rewrite

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(12)

Muroya (U. Birmingham) 8

Avoid re-evaluation: dynamic rewrite

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(13)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

9

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(14)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

9

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(15)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

9

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(16)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

10

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(17)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

10

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(18)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

11

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(19)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

11

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(20)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

11

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(21)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

12

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(22)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

12

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(23)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

13

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

(24)

Muroya (U. Birmingham)

Avoid re-evaluation: dynamic rewrite

13

↵ : ! : : Cut : : C+ :

i

: p ↵ : ! : : Cut :

i

: p

? ? ! C

k+1

Cut

~ C

· · ·

1

1

m

m

↵ "

1

· · ·

i

· · ·

k+1

G

· · ·

· · ·

? ? !

Cut

1

m

"

i

G

· · ·

· · ·

? ? ! C

k

Cut

~ C

· · ·

µ

1

µ

m

µ

1

· · ·

k+1

G ˜

· · ·

· · ·

1 m

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, Eit ‡ hE, A[V ]ic ‡ hA[V ]ia ‡ Call-by-need storeless abstract machine:

hV, Eit !need hE, V ic

hM N, Eit !need hM, E[[ ] N ]it

hM + N, Eit !need hM, E[[ ] + N ]it

hx, E1[let x = N in E2]it !need hN, E1[let x := [ ] in E2[x]]]it h[ ], A[V ]ic !need hA[V ]ia

hE[[ ] N ], A[ x. M ]ic !need hM [x0/x], E[A[let x0 = N in [ ]]]it hE[[ ] + N ], A[n]ic !need hN, E[A[n + [ ]]]it

hE[n + [ ]], A[m]ic !need hE, A[n + m]ic

hE[let x = N in [ ]], A[V ]ic !need hE, let x = N in A[V ]ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[let x = V in E0]], V ic

hE[let x := [ ] in E0[x]], A[V ]ic !need hE[A[E0]], V ic (if x does not appear in E0)

6

参照

関連したドキュメント

These analysis methods are applied to pre- dicting cutting error caused by thermal expansion and compression in machine tools.. The input variables are reduced from 32 points to

The Gaussian kernel is widely employed in Radial Basis Function (RBF) network, Support Vector Machine (SVM), Least Squares Support Vector Machine (LS-SVM), Kriging models, and so

Abstract The vehicle type auto-doffing system for the covering machine has been proposed in order to automate the preparation process of covered yarn.. In this report,

GoI token passing fixed graph.. B’ham.). Interaction abstract

Wu, “A generalisation model of learning and deteriorating effects on a single-machine scheduling with past-sequence-dependent setup times,” International Journal of Computer

So when these modified parts are ordered please inform the serial number of the sewing

interaction abstract machine token passing on fixed graph. call

In this study, the moving behavior and contact stress state of the ball pitched with the three rollers type pitching machine is analyzed using dynamic finite element analysis