# Tag Info

The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over. Let us compare the situation to the definite integral, for concretness just from $0$ to $1$. Here is an example: $$\int_0^1 x^2 + 3 x \, dx$$ This is a very archaic way of writing mathematical expressions that mathematicians like ...
The other answers are good, I just wanted to make it explicit that currying for dependent types is $$\textstyle \prod (x : A) . \prod (y : B(x)) . C(x, y) \ \cong \ \prod (p : \sum (x : A) . B(x)) . C(\pi_1(p), \pi_2(p))$$ which is more suggestive in Agda-style notation: $$(x : A) \to (y : B(x)) \to C(x,y) \ \cong\ (p : (x : A) \times B(x)) \to C(\pi_1(... 4 One answer is that we use English, but that's not what you're looking for. To make the question more precise, let us ask what sort of formalism is useful for describing logics. This is still quite broad, because a logic has several parts: syntax, rules of inference, semantics, etc. Syntax is pretty well understood and we know that the syntax of a language ... 3 The theory of higher-order critical pairs can indeed handle this example, as outlined in the following article: Higher-Order Rewrite Systems and their Confluence, Richard Mayr & Tobias Nipkow There are several different notions of higher-order rewrite systems, and several of them are able to handle your example, including those of the paper. The ... 2 I wouldn't consider it a higher-order function. A higher-order function takes a function as input, or yields a function as its output. In contrast, it sounds to me like your compiler extension is accepting data as input (the abstract syntax tree) and producing data on its output. I suppose you could consider the AST a specification of a function, but that ... 2 Generally you have: Some boolean variables that collectively represent the current state, say s,t,u. Some boolean variables that collectively represents the inputs, say i,j,k. For instance, you might have one variable per sensor (assuming each sensor returns a boolean value). Some boolean variables that collectively represents the inputs, say o,p,q. ... 2 As you may know, "interesting" classes of language often correspond to "interesting" classes of automata and also "interesting" algebras. For example, regular languages correspond to NFAs/DFAs, and Kleene algebras. It's the same with logic. Interesting logics often corresponding to interesting category structures, interesting programming languages, and so ... 2 The uncurrying process will lead to existential types. Since the adjoint of (X\to) is (X\times\vphantom{Y}) and the adjoint of (\forall X.) is (\exists X.), it is appearently inevitable. Also, it will lead to types depending on terms (where simple types only depends on types themselves, and polymorphism allows terms to depend on types). So generally ... 1 I can only think of some uncurrying of 1 and 3. \forall X. (X \times int) \rightarrow X It looks like we can not uncurry this one, unless we transform it first into the isomorphic type 1. int \rightarrow \forall X. (X \times int) \rightarrow X Alternatively, if we can apply an isomorphism, (3) can be rewritten as$$ \forall X. int \rightarrow (X \times ...