Everybody Loves Somebody

プログラミング

述語論理に限定継続を追加して、everybodyやsomebodyを表す項を作ってみる。

以下、{\bf C}, \langle \cdot \rangle はそれぞれ shift0, reset0 とする。

{\displaystyle e = {\bf C}k. \forall x. k \hookleftarrow x \\ s = {\bf C}l. \exists y. l \hookleftarrow y }

{\displaystyle \langle L(e, a) \rangle \\ = \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), a ) \rangle \\ \leadsto \forall x. \langle L( \square, a ) \rangle \hookleftarrow x \\ \leadsto \forall x. \langle L( x, a ) \rangle \\ \leadsto \forall x. L( x, a ) }

{\displaystyle \langle L(a, s) \rangle \\ = \langle L( a, ({\bf C}l. \exists y. l \hookleftarrow y) ) \rangle \\ \leadsto \exists y. \langle L( a, \square ) \rangle \hookleftarrow y \\ \leadsto \exists y. \langle L( a, y ) \rangle \\ \leadsto \exists y. L( a, y ) }

同時に複数使うと、引数を右から評価するか左から評価するかで継続が異なるため、結果が一意にならず、英語の表現と同様に曖昧になる。

左から評価すると：
{\displaystyle \langle L(e, s) \rangle \\ = \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), ({\bf C}l. \exists y. l \hookleftarrow y) ) \rangle \\ \leadsto \forall x. \langle L( \square, ({\bf C}k. \exists y. k \hookleftarrow y) ) \rangle \hookleftarrow x \\ \leadsto \forall x. \langle L( x, ({\bf C}k. \exists y. k \hookleftarrow y) ) \rangle \\ \leadsto \forall x. \exists y. \langle L( x, \square ) \rangle \hookleftarrow y \\ \leadsto \forall x. \exists y. \langle L( x, y ) \rangle \\ \leadsto \forall x. \exists y. L( x, y ) }

右から評価すると：
{\displaystyle \langle L(e, s) \rangle \\ = \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), ({\bf C}l. \exists y. l \hookleftarrow y) ) \rangle \\ \leadsto \exists y. \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), \square ) \rangle \hookleftarrow y \\ \leadsto \exists y. \langle L( ({\bf C}k. \forall x. k \hookleftarrow x), y ) \rangle \\ \leadsto \exists y. \forall x. \langle L( \square, y ) \rangle \hookleftarrow x \\ \leadsto \exists y. \forall x. \langle L( x, y ) \rangle \\ \leadsto \exists y. \forall x. L( x, y ) }

以下、Racketでの実装。

#lang racket
(require racket/control)

(define (forall x f) (if (null? x) #t (if (f (first x)) (forall (rest x) f) #f)))
(define (exists x f) (if (null? x) #f (if (f (first x)) #t (exists (rest x) f))))

(define (every x) (shift0 k (forall x k)))
(define (some x) (shift0 k (exists x k)))

(reset0 (even? (every '(10 20 30))))
(reset0 (even? (every '(10 20 5))))
(reset0 (even? (some '(5 7 9))))
(reset0 (even? (some '(5 7 10))))