[Richard Suchenwirth] 2002-05-15 - In [return], Lars Hellström used special return codes to handle questions like "for all a in A there exists some b in B such that for all c in C the condition P(a,b,c) holds". It appears as if the same task can be done with nested proc calls (and regular returns), while looking even more similar to the original task specification:
======
forall a $A {exists b $B {forall c $C {P $a $b $c}}}
======
The implementation is:
======
proc forall {elementName set condition} {
   upvar 1 $elementName element
      foreach element $set {
         if {![uplevel 1 $condition]} {return 0}
      }
   return 1
}
proc exists {elementName set condition} {
   upvar 1 $elementName element
      foreach element $set {
         if {[uplevel 1 $condition]} {return 1}
      }
   return 0

}
#--------------- self-test
if {[file tail [info script]]==[file tail $argv0]} {
   proc P {x y z} {
      expr {$x<3 && $y==5 && $z>6}
   }
   set A {1 2 3}
   set B {4 5 6}
   set C {7 8 9}
   set res [forall a $A {
      exists b $B {
         forall c $C {P $a $b $c}
      }
   }]
   puts res:$res 
}
======

''adapted from the chat:''

[dkf]: ''forall'' and ''exists'' are the classic operators of first-order logic (FOL) though they are obviously easy to lift to higher order logic (if you want to get more fun, try selecting the sets for the inner operations - or even snippets of Tcl code - using the outer operations)

[dkf]: The most useful way of doing things with forall/exists is to have a variable, a set, a selector (to restrict the set) and some general condition which we're testing forall/exists.

 forall A {{a b c} {b c d} {c d e}} {exists x $A {string equal $x "c"}} 
 forall A {equal match} {exists B {aaa a*} {string $A $B aaa}} 
 forall A {{string equal} {string match} regexp} {eval $A a a} 

----
[RS] has a feeling that this is structurally very similar to [KBK]'s code in [Solving Cryptarithms], on one hand, and to [Streams] on the other: nested uplevels, explicitly evalled, build up (mildly) complex structures of reasoning, logic, or data flow...
----
[aspect] is reminded of two procs I have in my prelude:
======
## WARNING: I do not endorse these implementations for use with >2 args.
## The signature in that case should probably be [all cmdPrefix ls ?ls ...?]

# all ?cmdPrefix ..? $ls
proc all {args} {
    set ls [lindex $args end]
    set cmd [lrange $args 0 end-1]
    if {$cmd eq ""} {
        set cmd K
    }
    foreach x $ls {
        if {![uplevel 1 {*}$cmd [list $x]]} {return false}
    }
    return true
}

# any ?cmdPrefix ..? $ls
proc any {args} {
    set ls [lindex $args end]
    set cmd [lrange $args 0 end-1]
    if {$cmd eq ""} {
        set cmd K
    }
    foreach x $ls {
        if {[uplevel 1 {*}$cmd [list $x]]} {return true}
    }
    return false
}
======
These permit an interesting implementation of the above:
======
proc forall {name set cond} {
   all [uplevel 1 [list lmap $name $set $cond]
}
proc forall {name set cond} {
   any [uplevel 1 [list lmap $name $set $cond]
}
======
With an implementation of [function composition], this approaches (modulo scope) the even simpler:  `interp alias {} forall {} {*}[compose all lmap]`, but the https://en.wikipedia.org/wiki/Curry-Howard_isomorphism%|%proof of this proposition%|% is unfortunately too large to http://mathworld.wolfram.com/FermatsLastTheorem.html%|%fit in this margin%|% (that is to say, my implementation of `compose` would draw in enough code to triple the length of this page and I'd have to introduce all the helpers - yuck).

----
[Playing predicate logic] | [Playing first-order logic] | [Arts and crafts of Tcl-Tk programming]