1
$\begingroup$

Observation:

  1. Sigma summation is iterative form of binary plus.
  2. Pi-capital product is iterative form of multiplication.
  3. Lattice supremum is iterative form binary meet.
  4. Lattice infinum is iterative form binary join.
  5. Existential and universal quatifiers are lattice supremum and infinum.
  6. Integral is summation "in the limit".

Does any quantifier have associated binary operation; for example what generalized quantifiers like "more than 5" corresponds to? Positive answer to this question would hint to binary operation corresponding to the limit quantifier -- essentially we are looking into where sequence "majority" leads to.

Likewise, what might be a binary operation corresponding to lambda abstraction? Having associated binary operation greatly facilitates intuition behind quantifier; it can be thought of as just repetitive application of binary operation.

  • 0
    $\forall$ is basically a big conjunction, and $\exists$ is basically a big disjunction. Lambda abstraction can be thought of as a kind of $\forall$.2012-06-14
  • 0
    Do I interpret you right when I suspect that when you say "any quantifier" you mean "every variable binder"? If so I think the finitary companion to a lambda abstraction would be the union operator for functions with disjoint domains.2012-06-14
  • 0
    Every variable binder would be too stringent, because there are many more binders than binary operations. For one thing, what properties do we expect from quantifier concept (in addition to variable binding)? Regarding union operator, can you please complete expression $ \lambda x . f(x) = $2012-06-14
  • 0
    @TegiriNenashi: Personally I only use the word "quantifier" for $\forall$ and $\exists$, but it seems like you're more liberal than that. It's your question, however, so it's your right and duty to define your terms. You can't just ask us to define what it is you meant.2012-06-14
  • 0
    @HenningMakholm: Can you please write something similar to $ \forall x P(x) = P(1) \wedge P(2) \wedge ...$ for lambda expression?2012-06-14
  • 0
    @Zhen: can you please be more specific? Then, what does your answer mean from duality perspective?2012-06-14
  • 3
    @TegiriNenashi: It would be something like $$\lambda x.x+2 = \{0\mapsto 2\}\uplus\{1 \mapsto 3\}\uplus \{2 \mapsto 4\}\uplus \cdots$$2012-06-14
  • 0
    @TegiriNenashi: Lambda abstraction doesn't really fit into your framework, as it operates on _terms_, not _formulae_.2012-06-14

0 Answers 0