Submissions/Deductive lambda calculus, logic, and functional programming

After careful consideration, the Programme Committee has decided not to accept the below submission at this time. Thank you to the author(s) for participating in the Wikimania 2014 programme submission, we hope to still see you at Wikimania this August.

Submission no. 9011

Deductive lambda calculus, logic, and functional programming

Type of submission

presentation:

Author of the submission

Thepigdog

E-mail address

peter.driscoll@dionglobal.com

Username

Thepigdog

Country of origin

Australia

Affiliation, if any

None

Personal homepage or blog

None

Abstract (at least 300 words to describe your proposal)

The fusion of logic and functional programming naturally requires the introduction of lambda abstractions into logic. But since the beginning, lambda calculus has had the cardinality problem (see Curry's paradox). This problem is related to the cardinality problem for inverse functions. Functions that are not 'one to one' have inverses that may have multiple or no values mapped to a given value. The solution to both cardinality problems is to keep the variable. Considered in another way the variable represents a named set of values which may be considered as a world set. Within the world set each value is in a world. The world may be considered as representing the possibility that the variable has the particular value. Multiple values may then be modeled as a single 'value' where each component value is tagged with an identifier representing the world. The result of this construction is similar to constraint logic programming, but simpler because the logic component may be modeled as functions on Booleans and there inverses. With multiple values for function inverses no longer being a problem the logic, or Boolean value component, becomes no different from any other type.

Because both functions and function inverses are supported, the language does not need to be based on solved equations. Any equation with a single instance of an unknown variable may be solved only by inverses. Instead of rearranging the equation, calculation proceeds starting from the requested value until known values are found. Whatever values are known determines the function, or function inverse required to calculate the unknown value. Calculation proceeds back from known values until the requested value may be calculated.

Lambda abstractions allow a function to be the requested value. So an equation may be considered as a definition of a function, and a lambda abstraction gives the solution. Where the function name is represented twice in the equation the function is recursive. It is then necessary to specify which function name instance we wish to solve for.

The result is a language based on functions and function inverses which has the cleanness of a functional language, with more than the power of a constraint logic programming language.

Track

Length of session (if other than 30 minutes, specify how long)

30 minutes

Will you attend Wikimania if your submission is not accepted?

No

Slides or further information (optional)

Special requests

Interested attendees

If you are interested in attending this session, please sign with your username below. This will help reviewers to decide which sessions are of high interest. Sign with a hash and four tildes. (# ~~~~).

1. Add your username here.