3
$\begingroup$

A partial function is one, that that is only defined on a part of its domain. Haskell gives examples: https://wiki.haskell.org/Partial_functions

My end goal is to express types

$$ \prod_{D:\mathcal{U}} D \qquad\qquad\qquad\qquad \prod_{\mathcal{A}:\mathfrak{A}} \mathcal{L}(\mathcal{A}) $$

  • The first type should simply represent sort of (polymorphic) choice functions which accecpt a type and return an element of that Type.
  • The second is assuming, that I can express the Type of Automata $\mathfrak{A}$ as well as the language $\mathcal{L}(\mathcal{A})$ accepted by automaton $\mathcal{A}$. Given an Automaton a function with the given pitype should Select a word accepted by it.

As far as I understand, in a basic dependently typed lambda calculus, both types suffer from the same problem: Their elements can never be introduced. Neither is it possible to select an element from the type $\bot$ nor select a word accepted by an automaton that doesn't accept any words.

I was wondering, if partial functions may be a solution to that problem. But how are partial functions are represented in a typed lambda calculus? An easy way I can imagine would be to be to create expressions, that allow the introduction of partial functions, such that there simply are no computation rules for undefined inputs.

So my questions are:

  • Does that make any sence, and is it common to solve this kind of problem that way? Is there good literature?
  • If the approach seems legit, is it possible to distinguish partial function types $A \rightharpoonup B$ from regular ones $A \to B$?

Note on the purpose: To be honest, I haven't formalized automata in any calculus, since for now I mostly would like to steal the concept and notation of dependent types and use them in my work to get across a concept. But if what i will do isn't completely bogus, it would maybe at least leave open a possibility to formalize things later.

A choice function of type $\prod_{D:\mathcal{U}} D$ is meant to represent user input - which should be non deterministic .. so there would also be no congruence)

  • Bonus question: Can non-deterministic functions be represented in a calculus such that this may be expressed?
$\endgroup$
2
$\begingroup$

It is possible to take a typed lambda calculus and add general recursion or fixed points. See for instance Plotkin's PCF, or HOFL in Winskel's formal semantics book.

In that way, one keeps the type system but introduces partiality. This is a very common approach for Turing complete typed programming languages.

Of course, now the logic associated to the calculus via Curry-Howard is no longer consistent, since every type is inhabited (by non terminating terms). This is not a serious problem for programming.

If wanted, in the type system one could distinguish between terms involving general recursion (which might not terminate), and terms involving no recursion or some known-to-be-terminating one, like (higher-order) primitive recursion. Note that this will not separate the programs between "halting" and "non-halting", which is undecidable, but only between "statically known to halt" and "statically unknown to halt -- they might or might not".

I have not thought much about that, but intuitively a non-termination monad would fit nicely in such type system. With a non-deterministic monad, one can also address non-deterministic functions.

A final comment: after reading the question, I am actually more concerned about the posted automaton-based example than termination. With dependent types, one can use the $\Pi$-type of a selection function (as the one which was posted), which given an automaton return one of the accepted strings (or a "empty-language" token). However, let's keep in mind that when a dependent type system checks a term against such $\Pi$-type, the term must contain the recipe to generate the string, as well as a proof that such string is accepted by the automaton. The posted question, in my view, seems to forget about that -- as if the type system could check any algorithm correct (in the sense of returning an accepted string). This is not possible.

$\endgroup$
  • 1
    $\begingroup$ I am not sure if I interpreted the question correctly, it seems a bit vague in some points. I'm hoping that the OP, reading this answer, can either confirm I read the question correctly, or clarify the points I misunderstood. $\endgroup$ – chi May 20 '17 at 18:26
  • $\begingroup$ Regarding the objection: emptiness of finite automata can be decided with bfs from initial to final states - so, given an automaton type can be expressed, shouldn't it also theoretically be possible, to formalize an acceptance test as well as an emptyness check that would do this? $\endgroup$ – IARI May 20 '17 at 22:47
  • $\begingroup$ @IARI That's not enough. We don't have a string $w$ and automaton $A$ to check. We only have a term, i.e. an algorithm $W(A)$, and we need to prove that for all automata $A$ it holds $W(A) \in L(A)$. Even if the term only had to decide emptiness, the type system would need to check that for every $A$, the term on $A$ reports "empty" iff $L(A)$ is indeed empty. Since we need to prove a "forall automata $A$ ..." property to check that the type is correct, standard automata decision procedures are not enough. $\endgroup$ – chi May 21 '17 at 7:31
  • $\begingroup$ That is true, and I have no idea if that actually possible. But could I theoretically introduce the language type on a meta level? I.e. define automata and give a rule for the type $\mathfrak{A} : \mathcal{U}$ of automata. $\endgroup$ – IARI May 25 '17 at 11:46
  • $\begingroup$ then define an accepting run $q_0\xrightarrow{w}q_f \in Q \times \Sigma^* \times Q$ in the automaton and then give a type rule: $\Gamma \vdash A : \mathfrak{A}$ implies $\Gamma \vdash \mathcal{L}(A) : \mathcal{U}$ and an introdoction: $\Gamma \vdash w : \mathcal{L}(A)$ if (meta) $q_0\xrightarrow{w}q_f \in Q \times \Sigma^* \times Q$ where $Q$ are the states and $\Sigma$ the alphabet in $A$... or something like that - (maybe even directly encode non-empty automata and save myself from the partial-function problem) $\endgroup$ – IARI May 25 '17 at 11:46
0
$\begingroup$

There is nothing that prevents dependent types from declaring:

$$T: a \rightarrow a \rightarrow bool$$

If you can then prove, or if you assume:

$$\forall x,y,z(T(x,y) \wedge T(x,z)\Rightarrow y=z)$$

You then know that $T$ is a partial function. You can then use a maybe type and define:

$$T(x,y) \Rightarrow t(x) = \mathbb{just}(y)$$

$$\neg \exists y T(x,y) \Rightarrow t(x) = \mathbb{nothing}$$

Which gives you a function of signature:

$$t:a \rightarrow \mathbb{maybe}\,a$$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.