Function pointer

Stream: general

[Sven Nilsen]

is there a function pointer type in Lean 4? in Rust there is fn(T) -> U and this allows adding axioms for meta theorem proving to Rust's type system. I am interested in porting some code from Rust to Lean 4.

[Arthur Paulino]

You can say f : T -> U

[Sven Nilsen]

T -> U in Lean 4 is the type of a lambda, that can capture variables from the environment. I need a function pointer that can not capture variables.

[Anatole Dedecker]

There is no internal notion of capture in Lean

[Anatole Dedecker]

What kind of things would you need this for?

[Sven Nilsen]

Exponential propositions: https://github.com/advancedresearch/path_semantics/blob/master/papers-wip2/hooo-exponential-propositions.pdf

[Sven Nilsen]

Lambdas are one kind of exponential object, but function pointer is another exponential object which is very useful for meta theorem proving. This allows extending Propositional Logic with exponential objects that behave like |- in Sequent Calculus

[Sven Nilsen]

It is also used to define path semantical qubit ~ which has tautological congruence instead of normal congruence. Under normal congruence, if a == b then f(a) == f(b), however, with tautological congruence you need (a == b)^true to prove f(a) == f(b). This is used by ~ to extend classical logic with probabilistic propositions, e.g. ~a gives a new proposition with the "source" a. I'm studying how logic behaves with extended operators ^ (exponential propositions) and ~ (called a "qubit").

[Sven Nilsen]

Currently, I am using an inductive type:

-- `a^b`.
-- Exponential (function pointer).
inductive FPow (a : Type u) (b : Type v)

-- `a^true`.
-- Tautology.
def Tauto a := FPow a Tr

-- `false^a`.
def Para a := FPow Fa a

-- `true^a`.
axiom tr a : FPow Tr a

-- `a^false`.
axiom fa a : FPow a Fa

-- `a^b & b => a`.
-- Modus ponens.
axiom modus_ponens {a b} (f : FPow a b) (x : b) : a

-- `a^true => a`.
theorem tauto {a} : Tauto a → a := fun x => modus_ponens x Tr.intro

However, I have to rewrite all statements that I want to hold tautologically using FPow, which is difficult. I haven't yet studied in detail what is required to implement this logic in a type system that doesn't distinguish between lambdas and function pointers.

[Anatole Dedecker]

Is there a key property that holds for one but not the other? Since I’m not familiar with Rust I’m having troubles understanding the subtlety

[Henrik Böving]

image.png

[Henrik Böving]

But no Lean doesn't have a function pointer concept distinct from lambdas right now. That said I believe it can be added in theory even though you have to be a bit careful as many lambdas end up being lambda lifted into actual functions so you can technically use them as function pointers. That said I don't understand how your formalization ends up resolving the context/closure issue. Since you are still creating objects within Lean of course there can always be an environment at play.

[Sven Nilsen]

If you have a type for function pointers in the type system, then you can write a proof of a => b and lift it to (a => b)^true. A such proof can use the global context. However, you can not do this with an argument of type a => b, because this argument might be the result of a runtime computation. The type system can not distinguish "impossible computations" from "possible computations" (those that are decidable). You have to "know" that the proof of a => b is provable. This is why one needs a type for function pointers. By adding a few axioms for meta theorem proving, one can construct "new function pointers" within the type system.

In Rust, Fn(T) -> U is the trait constraint of closure/lambdas. The fn(T) -> U type is for function pointers.

[Anatole Dedecker]

So you mean that, even with False in your context, you shouldn’t be able to prove (a -> b)^\top?

[Sven Nilsen]

with False in your context, you can prove anything, including (a => b)^true

[Sven Nilsen]

a type for function pointers is onto-logically a reference for a function pointer, not an "actual" function pointer. so, meta theorem proving is about proving statements about references.

[Timo Carlin-Burns]

If I'm understanding correctly, the key difference is in what you know if you take x^true as a hypothesis. Let's say we have a proof in our context that ((a = b)^true) -> ((b = a)^true). This implication takes an exponential as a hypothesis. We can only use the implication if we supply it a proof of (a = b)^true, a proof of a = b from an empty context. If we also have false in our context and use it to prove a = b, then we only have (a = b)^false, so we can't use the implication.

[Sven Nilsen]

x^false is provable for any x, so you can prove ((b == a)^true)^false and then lift it to (((a = b)^true) => ((b = a)^true))^false (you can also do this directly). so, if you have false in your context, then you can prove any theorem.

[Sven Nilsen]

The key difference is that a == b can happen at runtime, e.g. by faulty hardware and prove an unsound theorem. This is an "impossible computation" seen from the perspective of compile time. (a == b)^true is a reference to a == b as provable at compile time.

[Sven Nilsen]

When we say a == b in logic, we do not exclude possibilities that this might become true at some point in the future, by making further assumptions. We do not express under which circumstances such assumptions might be made. When using a single type for lambdas and function pointers, the runtime and compile time gets collapsed into one semantical level. You need a stronger theory of reference to talk about compile time explicitly. The normal procedure to handle this is by enforcing rigor through the use of the language, instead of through the type system.

The reason Rust added a separate type for function pointers, was because of performance concerns. A closure/lambda needs extra memory at runtime, while function pointers can be passed around in a single hardware depending usize.

[Schrodinger ZHU Yifan]

Interestingly, I noticed a problem related to this in LeanGccJit:

When a foreign function pointer is passed to lean (say, we compiled a function with LeanGccJit), lean actually have no way to invoke it inside its own runtime environment because there is no raw function pointer.

One may workaround this by porting lean runtime into LeanGccJit context and wrap a closure that conforms the uniform ABI.